lemmas atomize = all_eq imp_eq;
authorwenzelm
Fri Aug 04 22:56:52 2000 +0200 (2000-08-04)
changeset 9529d9434a9277a4
parent 9528 95852b4be214
child 9530 f0ffd29fd4e4
lemmas atomize = all_eq imp_eq;
setup hypsubst_setup;
src/HOL/HOL.thy
     1.1 --- a/src/HOL/HOL.thy	Fri Aug 04 22:56:31 2000 +0200
     1.2 +++ b/src/HOL/HOL.thy	Fri Aug 04 22:56:52 2000 +0200
     1.3 @@ -192,7 +192,7 @@
     1.4  (* theory and package setup *)
     1.5  
     1.6  use "HOL_lemmas.ML"	setup attrib_setup
     1.7 -use "cladata.ML"	setup Classical.setup setup clasetup
     1.8 +use "cladata.ML"	setup hypsubst_setup setup Classical.setup setup clasetup
     1.9  
    1.10  lemma all_eq: "(!!x. P x) == Trueprop (ALL x. P x)"
    1.11  proof (rule equal_intr_rule)
    1.12 @@ -213,6 +213,8 @@
    1.13    thus B ..
    1.14  qed
    1.15  
    1.16 +lemmas atomize = all_eq imp_eq
    1.17 +
    1.18  use "blastdata.ML"	setup Blast.setup
    1.19  use "simpdata.ML"	setup Simplifier.setup
    1.20  			setup "Simplifier.method_setup Splitter.split_modifiers"