diff -r ee360f910ec8 -r 0760eda193c4 src/FOL/FOL.thy
--- 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);
 *}