--- a/src/HOL/equalities.ML Wed Sep 29 14:36:36 1999 +0200
+++ b/src/HOL/equalities.ML Wed Sep 29 14:38:03 1999 +0200
@@ -160,7 +160,7 @@
qed "Int_assoc";
(*Intersection is an AC-operator*)
-val Int_ac = [Int_assoc, Int_left_absorb, Int_commute, Int_left_commute];
+bind_thms ("Int_ac", [Int_assoc, Int_left_absorb, Int_commute, Int_left_commute]);
Goal "B<=A ==> A Int B = B";
by (Blast_tac 1);
@@ -240,7 +240,7 @@
qed "Un_assoc";
(*Union is an AC-operator*)
-val Un_ac = [Un_assoc, Un_left_absorb, Un_commute, Un_left_commute];
+bind_thms ("Un_ac", [Un_assoc, Un_left_absorb, Un_commute, Un_left_commute]);
Goal "A<=B ==> A Un B = B";
by (Blast_tac 1);
@@ -436,7 +436,7 @@
(*Basic identities*)
-val not_empty = prove_goal Set.thy "(A ~= {}) = (? x. x:A)" (K [Blast_tac 1]);
+bind_thm ("not_empty", prove_goal Set.thy "(A ~= {}) = (? x. x:A)" (K [Blast_tac 1]));
Goal "(UN x:{}. B x) = {}";
by (Blast_tac 1);
@@ -896,4 +896,11 @@
end;
+bind_thms ("UN_simps", UN_simps);
+bind_thms ("INT_simps", INT_simps);
+bind_thms ("ball_simps", ball_simps);
+bind_thms ("bex_simps", bex_simps);
+bind_thm ("ball_conj_distrib", ball_conj_distrib);
+bind_thm ("bex_disj_distrib", bex_disj_distrib);
+
Addsimps (UN_simps @ INT_simps @ ball_simps @ bex_simps);
--- 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 ())