src/HOL/simpdata.ML
changeset 7648 8258b93cdd32
parent 7623 23efbb7ab889
child 7711 4dae7a4fceaf
--- a/src/HOL/simpdata.ML	Wed Sep 29 14:36:36 1999 +0200
+++ b/src/HOL/simpdata.ML	Wed Sep 29 14:38:03 1999 +0200
@@ -161,7 +161,7 @@
         (fn _=> [(Blast_tac 1)]) RS mp RS mp);
 
 (*Miniscoping: pushing in existential quantifiers*)
-val ex_simps = map prover 
+val ex_simps = map prover
                 ["(EX x. P x & Q)   = ((EX x. P x) & Q)",
                  "(EX x. P & Q x)   = (P & (EX x. Q x))",
                  "(EX x. P x | Q)   = ((EX x. P x) | Q)",
@@ -192,6 +192,10 @@
 
 end;
 
+bind_thms ("ex_simps", ex_simps);
+bind_thms ("all_simps", all_simps);
+
+
 (* Elimination of True from asumptions: *)
 
 val True_implies_equals = prove_goal (the_context ())