tuned;

--- a/src/HOL/HOL.thy	Sat Apr 04 22:22:38 2015 +0200
+++ b/src/HOL/HOL.thy	Mon Apr 06 12:37:21 2015 +0200
@@ -1365,44 +1365,32 @@
 subsubsection {* Generic cases and induction *}
 
 text {* Rule projections: *}
-
 ML {*
 structure Project_Rule = Project_Rule
 (
   val conjunct1 = @{thm conjunct1}
   val conjunct2 = @{thm conjunct2}
   val mp = @{thm mp}
-)
+);
 *}
 
-definition induct_forall where
-  "induct_forall P == \<forall>x. P x"
-
-definition induct_implies where
-  "induct_implies A B == A \<longrightarrow> B"
-
-definition induct_equal where
-  "induct_equal x y == x = y"
+definition "induct_forall P \<equiv> \<forall>x. P x"
+definition "induct_implies A B \<equiv> A \<longrightarrow> B"
+definition "induct_equal x y \<equiv> x = y"
+definition "induct_conj A B \<equiv> A \<and> B"
+definition "induct_true \<equiv> True"
+definition "induct_false \<equiv> False"
 
-definition induct_conj where
-  "induct_conj A B == A \<and> B"
-
-definition induct_true where
-  "induct_true == True"
-
-definition induct_false where
-  "induct_false == False"
-
-lemma induct_forall_eq: "(!!x. P x) == Trueprop (induct_forall (\<lambda>x. P x))"
+lemma induct_forall_eq: "(\<And>x. P x) \<equiv> Trueprop (induct_forall (\<lambda>x. P x))"
   by (unfold atomize_all induct_forall_def)
 
-lemma induct_implies_eq: "(A ==> B) == Trueprop (induct_implies A B)"
+lemma induct_implies_eq: "(A \<Longrightarrow> B) \<equiv> Trueprop (induct_implies A B)"
   by (unfold atomize_imp induct_implies_def)
 
-lemma induct_equal_eq: "(x == y) == Trueprop (induct_equal x y)"
+lemma induct_equal_eq: "(x \<equiv> y) \<equiv> Trueprop (induct_equal x y)"
   by (unfold atomize_eq induct_equal_def)
 
-lemma induct_conj_eq: "(A &&& B) == Trueprop (induct_conj A B)"
+lemma induct_conj_eq: "(A &&& B) \<equiv> Trueprop (induct_conj A B)"
   by (unfold atomize_conj induct_conj_def)
 
 lemmas induct_atomize' = induct_forall_eq induct_implies_eq induct_conj_eq
@@ -1413,7 +1401,6 @@
   induct_forall_def induct_implies_def induct_equal_def induct_conj_def
   induct_true_def induct_false_def
 
-
 lemma induct_forall_conj: "induct_forall (\<lambda>x. induct_conj (A x) (B x)) =
     induct_conj (induct_forall A) (induct_forall B)"
   by (unfold induct_forall_def induct_conj_def) iprover
@@ -1422,13 +1409,15 @@
     induct_conj (induct_implies C A) (induct_implies C B)"
   by (unfold induct_implies_def induct_conj_def) iprover
 
-lemma induct_conj_curry: "(induct_conj A B ==> PROP C) == (A ==> B ==> PROP C)"
+lemma induct_conj_curry: "(induct_conj A B \<Longrightarrow> PROP C) \<equiv> (A \<Longrightarrow> B \<Longrightarrow> PROP C)"
 proof
-  assume r: "induct_conj A B ==> PROP C" and A B
-  show "PROP C" by (rule r) (simp add: induct_conj_def `A` `B`)
+  assume r: "induct_conj A B \<Longrightarrow> PROP C"
+  assume ab: A B
+  show "PROP C" by (rule r) (simp add: induct_conj_def ab)
 next
-  assume r: "A ==> B ==> PROP C" and "induct_conj A B"
-  show "PROP C" by (rule r) (simp_all add: `induct_conj A B` [unfolded induct_conj_def])
+  assume r: "A \<Longrightarrow> B \<Longrightarrow> PROP C"
+  assume ab: "induct_conj A B"
+  show "PROP C" by (rule r) (simp_all add: ab [unfolded induct_conj_def])
 qed
 
 lemmas induct_conj = induct_forall_conj induct_implies_conj induct_conj_curry
@@ -1484,52 +1473,54 @@
 
 text {* Pre-simplification of induction and cases rules *}
 
-lemma [induct_simp]: "(!!x. induct_equal x t ==> PROP P x) == PROP P t"
+lemma [induct_simp]: "(\<And>x. induct_equal x t \<Longrightarrow> PROP P x) \<equiv> PROP P t"
   unfolding induct_equal_def
 proof
-  assume R: "!!x. x = t ==> PROP P x"
-  show "PROP P t" by (rule R [OF refl])
+  assume r: "\<And>x. x = t \<Longrightarrow> PROP P x"
+  show "PROP P t" by (rule r [OF refl])
 next
-  fix x assume "PROP P t" "x = t"
+  fix x
+  assume "PROP P t" "x = t"
   then show "PROP P x" by simp
 qed
 
-lemma [induct_simp]: "(!!x. induct_equal t x ==> PROP P x) == PROP P t"
+lemma [induct_simp]: "(\<And>x. induct_equal t x \<Longrightarrow> PROP P x) \<equiv> PROP P t"
   unfolding induct_equal_def
 proof
-  assume R: "!!x. t = x ==> PROP P x"
-  show "PROP P t" by (rule R [OF refl])
+  assume r: "\<And>x. t = x \<Longrightarrow> PROP P x"
+  show "PROP P t" by (rule r [OF refl])
 next
-  fix x assume "PROP P t" "t = x"
+  fix x
+  assume "PROP P t" "t = x"
   then show "PROP P x" by simp
 qed
 
-lemma [induct_simp]: "(induct_false ==> P) == Trueprop induct_true"
+lemma [induct_simp]: "(induct_false \<Longrightarrow> P) \<equiv> Trueprop induct_true"
   unfolding induct_false_def induct_true_def
   by (iprover intro: equal_intr_rule)
 
-lemma [induct_simp]: "(induct_true ==> PROP P) == PROP P"
+lemma [induct_simp]: "(induct_true \<Longrightarrow> PROP P) \<equiv> PROP P"
   unfolding induct_true_def
 proof
-  assume R: "True \<Longrightarrow> PROP P"
-  from TrueI show "PROP P" by (rule R)
+  assume "True \<Longrightarrow> PROP P"
+  then show "PROP P" using TrueI .
 next
   assume "PROP P"
   then show "PROP P" .
 qed
 
-lemma [induct_simp]: "(PROP P ==> induct_true) == Trueprop induct_true"
+lemma [induct_simp]: "(PROP P \<Longrightarrow> induct_true) \<equiv> Trueprop induct_true"
   unfolding induct_true_def
   by (iprover intro: equal_intr_rule)
 
-lemma [induct_simp]: "(!!x. induct_true) == Trueprop induct_true"
+lemma [induct_simp]: "(\<And>x. induct_true) \<equiv> Trueprop induct_true"
   unfolding induct_true_def
   by (iprover intro: equal_intr_rule)
 
-lemma [induct_simp]: "induct_implies induct_true P == P"
+lemma [induct_simp]: "induct_implies induct_true P \<equiv> P"
   by (simp add: induct_implies_def induct_true_def)
 
-lemma [induct_simp]: "(x = x) = True"
+lemma [induct_simp]: "x = x \<longleftrightarrow> True"
   by (rule simp_thms)
 
 hide_const induct_forall induct_implies induct_equal induct_conj induct_true induct_false

--- a/src/Tools/induct.ML	Sat Apr 04 22:22:38 2015 +0200
+++ b/src/Tools/induct.ML	Mon Apr 06 12:37:21 2015 +0200
@@ -162,7 +162,7 @@
 
 val rearrange_eqs_simproc =
   Simplifier.simproc_global Pure.thy "rearrange_eqs" ["Pure.all t"]
-    (fn ctxt => fn t => mk_swap_rrule ctxt (Thm.global_cterm_of (Proof_Context.theory_of ctxt) t));
+    (fn ctxt => fn t => mk_swap_rrule ctxt (Thm.cterm_of ctxt t));
 
 
 (* rotate k premises to the left by j, skipping over first j premises *)
@@ -515,7 +515,7 @@
 
 (** induct method **)
 
-val conjunction_congs = [@{thm Pure.all_conjunction}, @{thm imp_conjunction}];
+val conjunction_congs = @{thms Pure.all_conjunction imp_conjunction};
 
 
 (* atomize *)
@@ -549,7 +549,7 @@
   rewrite_goal_tac ctxt (Induct_Args.rulify @ conjunction_congs) THEN'
   rewrite_goal_tac ctxt Induct_Args.rulify_fallback THEN'
   Goal.conjunction_tac THEN_ALL_NEW
-  (rewrite_goal_tac ctxt [@{thm Pure.conjunction_imp}] THEN' Goal.norm_hhf_tac ctxt);
+  (rewrite_goal_tac ctxt @{thms Pure.conjunction_imp} THEN' Goal.norm_hhf_tac ctxt);
 
 
 (* prepare rule *)