From ff95b7b5113121d06662ed1508e90fadeb05c161 Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Sun, 17 Feb 2019 23:13:57 +0100
Subject: finalize quantify methods

---
 Prod.thy | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

(limited to 'Prod.thy')

diff --git a/Prod.thy b/Prod.thy
index a843c7a..ff62ee6 100644
--- a/Prod.thy
+++ b/Prod.thy
@@ -75,7 +75,7 @@ section \<open>Universal quantification\<close>
 text \<open>
 It will often be useful to convert a proof goal asserting the inhabitation of a dependent product to one that instead uses Pure universal quantification.
 
-Method @{theory_text quantify} converts the goal
+Method @{theory_text quantify_all} converts the goal
 @{text "t: \<Prod>x1: A1. ... \<Prod>xn: An. B x1 ... xn"},
 where @{term B} is not a product, to
 @{text "\<And>x1 ... xn . \<lbrakk>x1: A1; ...; xn: An\<rbrakk> \<Longrightarrow> ?b x1 ... xn: B x1 ... xn"}.
@@ -83,9 +83,8 @@ where @{term B} is not a product, to
 Method @{theory_text "quantify k"} does the same, but only for the first k unknowns.
 \<close>
 
-method_setup quantify = \<open>repeat (fn ctxt => Method.rule_tac ctxt [@{thm Prod_intro}] [] 1)\<close>
-
 method quantify_all = (rule Prod_intro)+
+method_setup quantify = \<open>repeat (fn ctxt => Method.rule_tac ctxt [@{thm Prod_intro}] [] 1)\<close>
 
 
 section \<open>Function composition\<close>
-- 
cgit v1.2.3