diff -r 385d51d74f71 -r 194d088c1511 equalities.ML
--- 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,