Updated simpsets and a few proofs.
Reomved junk file test.ML.

--- a/Nat.ML	Tue Mar 22 08:28:31 1994 +0100
+++ b/Nat.ML	Tue Mar 22 08:31:58 1994 +0100
@@ -425,3 +425,5 @@
 by (EVERY1[dtac le_imp_less_or_eq, dtac le_imp_less_or_eq,
           fast_tac (HOL_cs addEs [less_anti_refl,less_anti_sym])]);
 val le_anti_sym = result();
+
+val nat_ss = nat_ss addsimps [le_refl];

--- 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,

--- a/nat.ML	Tue Mar 22 08:28:31 1994 +0100
+++ b/nat.ML	Tue Mar 22 08:31:58 1994 +0100
@@ -425,3 +425,5 @@
 by (EVERY1[dtac le_imp_less_or_eq, dtac le_imp_less_or_eq,
           fast_tac (HOL_cs addEs [less_anti_refl,less_anti_sym])]);
 val le_anti_sym = result();
+
+val nat_ss = nat_ss addsimps [le_refl];

--- a/simpdata.ML	Tue Mar 22 08:28:31 1994 +0100
+++ b/simpdata.ML	Tue Mar 22 08:31:58 1994 +0100
@@ -69,6 +69,9 @@
 in
 
 val conj_assoc = prover "((P&Q)&R) = (P&(Q&R))";
+val conj_commute = prover "(P&Q) = (Q&P)";
+val conj_right_commute = prover "((P&Q)&R) = ((P&R)&Q)";
+val conj_ac = [conj_assoc RS sym, conj_commute, conj_right_commute];
 
 val if_True = prove_goal HOL.thy "if(True,x,y) = x"
  (fn _=>[stac if_def 1,  fast_tac (HOL_cs addIs [select_equality]) 1]);

--- a/subset.ML	Tue Mar 22 08:28:31 1994 +0100
+++ b/subset.ML	Tue Mar 22 08:31:58 1994 +0100
@@ -12,13 +12,6 @@
 val subset_insertI = prove_goal Set.thy "B <= insert(a,B)"
  (fn _=> [ (rtac subsetI 1), (etac insertI2 1) ]);
 
-(*Useful for rewriting!*)
-goalw Set.thy [subset_def,Ball_def] "insert(a,B)<=C = (a:C & B<=C)";
-(*by(SIMP_TAC (HOL_ss addsimps [insert_iff]) 1);*)
-by(simp_tac (HOL_ss addsimps [insert_iff]) 1);
-by(fast_tac HOL_cs 1);
-val insert_subset_iff = result();
-
 (*** Big Union -- least upper bound of a set  ***)
 
 val prems = goal Set.thy