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