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