--- a/src/LCF/LCF.thy Tue Nov 11 11:41:58 2014 +0100
+++ b/src/LCF/LCF.thy Tue Nov 11 11:47:53 2014 +0100
@@ -318,15 +318,15 @@
adm_not_free adm_eq adm_less adm_not_less
adm_not_eq_tr adm_conj adm_disj adm_imp adm_all
-
-ML {*
- fun induct_tac ctxt v i =
- res_inst_tac ctxt [(("f", 0), v)] @{thm induct} i THEN
- REPEAT (resolve_tac @{thms adm_lemmas} i)
+method_setup induct = {*
+ Scan.lift Args.name >> (fn v => fn ctxt =>
+ SIMPLE_METHOD' (fn i =>
+ res_inst_tac ctxt [(("f", 0), v)] @{thm induct} i THEN
+ REPEAT (resolve_tac @{thms adm_lemmas} i)))
*}
lemma least_FIX: "f(p) = p ==> FIX(f) << p"
- apply (tactic {* induct_tac @{context} "f" 1 *})
+ apply (induct f)
apply (rule minimal)
apply (intro strip)
apply (erule subst)
--- a/src/LCF/ex/Ex1.thy Tue Nov 11 11:41:58 2014 +0100
+++ b/src/LCF/ex/Ex1.thy Tue Nov 11 11:47:53 2014 +0100
@@ -28,7 +28,7 @@
done
lemma H_idemp_lemma: "ALL x. H(FIX(K,x)) = FIX(K,x)"
- apply (tactic {* induct_tac @{context} "K" 1 *})
+ apply (induct K)
apply simp
apply (simp split: COND_cases_iff)
apply (intro strip)
--- a/src/LCF/ex/Ex2.thy Tue Nov 11 11:41:58 2014 +0100
+++ b/src/LCF/ex/Ex2.thy Tue Nov 11 11:47:53 2014 +0100
@@ -19,7 +19,7 @@
lemma example: "ALL x. F(H(x::'a,y::'b)) = H(x,F(y))"
apply (simplesubst H)
- apply (tactic {* induct_tac @{context} "K:: ('a=>'b=>'b) => ('a=>'b=>'b)" 1 *})
+ apply (induct "K:: ('a=>'b=>'b) => ('a=>'b=>'b)")
apply simp
apply (simp split: COND_cases_iff)
done
--- a/src/LCF/ex/Ex3.thy Tue Nov 11 11:41:58 2014 +0100
+++ b/src/LCF/ex/Ex3.thy Tue Nov 11 11:47:53 2014 +0100
@@ -14,7 +14,7 @@
declare p_strict [simp] p_s [simp]
lemma example: "p(FIX(s),y) = FIX(s)"
- apply (tactic {* induct_tac @{context} "s" 1 *})
+ apply (induct s)
apply simp
apply simp
done
--- a/src/LCF/ex/Ex4.thy Tue Nov 11 11:41:58 2014 +0100
+++ b/src/LCF/ex/Ex4.thy Tue Nov 11 11:47:53 2014 +0100
@@ -10,7 +10,7 @@
shows "FIX(f)=p"
apply (unfold eq_def)
apply (rule conjI)
- apply (tactic {* induct_tac @{context} "f" 1 *})
+ apply (induct f)
apply (rule minimal)
apply (intro strip)
apply (rule less_trans)