--- a/equalities.ML Tue Mar 22 08:28:31 1994 +0100
+++ b/equalities.ML Tue Mar 22 08:31:58 1994 +0100
@@ -26,6 +26,10 @@
by (fast_tac eq_cs 1);
val insert_absorb = result();
+goal Set.thy "(insert(x,A) <= B) = (x:B & A <= B)";
+by (fast_tac set_cs 1);
+val insert_subset = result();
+
(** Image **)
goal Set.thy "f``{} = {}";
@@ -273,7 +277,7 @@
val Diff_Int = result();
val set_ss = set_ss addsimps
- [in_empty,in_insert,
+ [in_empty,in_insert,insert_subset,
Int_absorb,Int_empty_left,Int_empty_right,
Un_absorb,Un_empty_left,Un_empty_right,
constant_UN,image_empty,