diff options
| -rw-r--r-- | Prod.thy | 5 |
1 files changed, 2 insertions, 3 deletions
@@ -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> |