# HG changeset patch
# User wenzelm
# Date 965422489 -7200
# Node ID 46fb9ccae463c8ba69043abfade166ab7caba73d
# Parent  5721615da108beb69c20ac8ac4fa546c9494c1da
lemmas atomize = all_eq imp_eq;

diff -r 5721615da108 -r 46fb9ccae463 src/FOL/FOL.thy
--- 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"