lemmas atomize = all_eq imp_eq;

--- a/src/FOL/FOL.thy	Fri Aug 04 22:54:34 2000 +0200
+++ b/src/FOL/FOL.thy	Fri Aug 04 22:54:49 2000 +0200
@@ -47,6 +47,8 @@
   thus B ..
 qed
 
+lemmas atomize = all_eq imp_eq
+
 use "blastdata.ML"
 setup Blast.setup
 use "FOL_lemmas2.ML"