induct method: localize rews for rule;

--- a/src/FOL/FOL.thy	Mon Nov 19 17:42:00 2001 +0100
+++ b/src/FOL/FOL.thy	Mon Nov 19 20:46:05 2001 +0100
@@ -65,6 +65,9 @@
 lemmas induct_rulify1 [symmetric, standard] = induct_forall_eq induct_implies_eq induct_equal_eq
 lemmas induct_rulify2 = induct_forall_def induct_implies_def induct_equal_def
 
+lemma all_conj_eq: "(ALL x. P(x)) & (ALL y. Q(y)) == (ALL x y. P(x) & Q(y))"
+  by simp
+
 hide const induct_forall induct_implies induct_equal
 
 
@@ -75,12 +78,13 @@
   (struct
     val dest_concls = FOLogic.dest_concls;
     val cases_default = thm "case_split";
-    val local_imp_def = thm "induct_implies_def";
     val local_impI = thm "induct_impliesI";
     val conjI = thm "conjI";
     val atomize = thms "induct_atomize";
     val rulify1 = thms "induct_rulify1";
     val rulify2 = thms "induct_rulify2";
+    val localize = [Thm.symmetric (thm "induct_implies_def"),
+      Thm.symmetric (thm "atomize_all"), thm "all_conj_eq"];
   end);
 *}
 

--- a/src/HOL/HOL.thy	Mon Nov 19 17:42:00 2001 +0100
+++ b/src/HOL/HOL.thy	Mon Nov 19 20:46:05 2001 +0100
@@ -321,12 +321,12 @@
   (struct
     val dest_concls = HOLogic.dest_concls;
     val cases_default = thm "case_split";
-    val local_imp_def = thm "induct_implies_def";
     val local_impI = thm "induct_impliesI";
     val conjI = thm "conjI";
     val atomize = thms "induct_atomize";
     val rulify1 = thms "induct_rulify1";
     val rulify2 = thms "induct_rulify2";
+    val localize = [Thm.symmetric (thm "induct_implies_def")];
   end);
 *}
 

--- a/src/Provers/induct_method.ML	Mon Nov 19 17:42:00 2001 +0100
+++ b/src/Provers/induct_method.ML	Mon Nov 19 20:46:05 2001 +0100
@@ -10,12 +10,12 @@
 sig
   val dest_concls: term -> term list
   val cases_default: thm
-  val local_imp_def: thm
   val local_impI: thm
   val conjI: thm
   val atomize: thm list
   val rulify1: thm list
   val rulify2: thm list
+  val localize: thm list
 end;
 
 signature INDUCT_METHOD =
@@ -150,7 +150,7 @@
   Tactic.rewrite_goal_tac Data.rulify2 THEN'
   Tactic.norm_hhf_tac;
 
-val localize = Tactic.simplify false [Thm.symmetric Data.local_imp_def];
+val localize = Tactic.norm_hhf o Tactic.simplify false Data.localize;
 
 
 (* imp_intr --- limited to atomic prems *)