subset.ML

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