--- a/src/HOL/HOL.thy Fri Aug 04 22:56:31 2000 +0200
+++ b/src/HOL/HOL.thy Fri Aug 04 22:56:52 2000 +0200
@@ -192,7 +192,7 @@
(* theory and package setup *)
use "HOL_lemmas.ML" setup attrib_setup
-use "cladata.ML" setup Classical.setup setup clasetup
+use "cladata.ML" setup hypsubst_setup setup Classical.setup setup clasetup
lemma all_eq: "(!!x. P x) == Trueprop (ALL x. P x)"
proof (rule equal_intr_rule)
@@ -213,6 +213,8 @@
thus B ..
qed
+lemmas atomize = all_eq imp_eq
+
use "blastdata.ML" setup Blast.setup
use "simpdata.ML" setup Simplifier.setup
setup "Simplifier.method_setup Splitter.split_modifiers"