--- a/subset.ML Thu Nov 24 20:31:09 1994 +0100
+++ b/subset.ML Fri Nov 25 09:12:16 1994 +0100
@@ -9,7 +9,7 @@
(*** insert ***)
-val subset_insertI = prove_goal Set.thy "B <= insert(a,B)"
+qed_goal "subset_insertI" Set.thy "B <= insert(a,B)"
(fn _=> [ (rtac subsetI 1), (etac insertI2 1) ]);
(*** Big Union -- least upper bound of a set ***)
@@ -117,7 +117,7 @@
(*** Set difference ***)
-val Diff_subset = prove_goal Set.thy "A-B <= (A::'a set)"
+qed_goal "Diff_subset" Set.thy "A-B <= (A::'a set)"
(fn _ => [ (REPEAT (ares_tac [subsetI] 1 ORELSE etac DiffE 1)) ]);
(*** Monotonicity ***)