# HG changeset patch
# User wenzelm
# Date 965422612 -7200
# Node ID d9434a9277a4d6644a6faf9faecb6ac214d6aba6
# Parent  95852b4be2147e69ba409f1018340ab4d6f719c5
lemmas atomize = all_eq imp_eq;
setup hypsubst_setup;

diff -r 95852b4be214 -r d9434a9277a4 src/HOL/HOL.thy
--- 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"