src/HOL/ex/set.ML

--- a/src/HOL/ex/set.ML	Mon Nov 03 12:12:10 1997 +0100
+++ b/src/HOL/ex/set.ML	Mon Nov 03 12:13:18 1997 +0100
@@ -16,7 +16,7 @@
 let val insertCI' = read_instantiate [("'a", "?'a set")] insertCI
 in    (*Type instantiation is required so that blast_tac can apply equalityI
         to the subgoal arising from insertCI*)
-by(blast_tac (!claset addSIs [insertCI']) 1)
+by(blast_tac (claset() addSIs [insertCI']) 1)
 end;
 
 (*** A unique fixpoint theorem --- fast/best/meson all fail ***)
@@ -30,12 +30,12 @@
 
 goal Set.thy "~ (? f:: 'a=>'a set. ! S. ? x. f(x) = S)";
 (*requires best-first search because it is undirectional*)
-by (best_tac (!claset addSEs [equalityCE]) 1);
+by (best_tac (claset() addSEs [equalityCE]) 1);
 qed "cantor1";
 
 (*This form displays the diagonal term*)
 goal Set.thy "! f:: 'a=>'a set. ! x. f(x) ~= ?S(f)";
-by (best_tac (!claset addSEs [equalityCE]) 1);
+by (best_tac (claset() addSEs [equalityCE]) 1);
 uresult();
 
 (*This form exploits the set constructs*)
@@ -49,14 +49,14 @@
 by (assume_tac 1);
 
 choplev 0;
-by (best_tac (!claset addSEs [equalityCE]) 1);
+by (best_tac (claset() addSEs [equalityCE]) 1);
 
 (*** The Schroder-Berstein Theorem ***)
 
 goalw Lfp.thy [image_def] "!!f. inj(f) ==> inv(f)``(f``X) = X";
 by (rtac equalityI 1);
-by (fast_tac (!claset addEs [inv_f_f RS ssubst]) 1);
-by (fast_tac (!claset addEs [inv_f_f RS ssubst]) 1);
+by (fast_tac (claset() addEs [inv_f_f RS ssubst]) 1);
+by (fast_tac (claset() addEs [inv_f_f RS ssubst]) 1);
 qed "inv_image_comp";
 
 goal Set.thy "!!f. f(a) ~: (f``X) ==> a~:X";
@@ -77,7 +77,7 @@
 
 goalw Lfp.thy [image_def]
     "range(%z. if z:X then f(z) else g(z)) = f``X Un g``Compl(X)";
-by (simp_tac (!simpset addsplits [expand_if]) 1);
+by (simp_tac (simpset() addsplits [expand_if]) 1);
 by (Blast_tac 1);
 qed "range_if_then_else";
 
@@ -86,7 +86,7 @@
 qed "X_Un_Compl";
 
 goalw Lfp.thy [surj_def] "surj(f) = (!a. a : range(f))";
-by (fast_tac (!claset addEs [ssubst]) 1);
+by (fast_tac (claset() addEs [ssubst]) 1);
 qed "surj_iff_full_range";
 
 val [compl] = goal Lfp.thy
@@ -107,9 +107,9 @@
 by (rewtac inj_def);
 by (cut_facts_tac [injf,injg] 1);
 by (EVERY1 [rtac allI, rtac allI, stac expand_if, rtac conjI, stac expand_if]);
-by (fast_tac (!claset addEs  [inj_ontoD, sym RS f_eq_gE]) 1);
+by (fast_tac (claset() addEs  [inj_ontoD, sym RS f_eq_gE]) 1);
 by (stac expand_if 1);
-by (fast_tac (!claset addEs  [inj_ontoD, f_eq_gE]) 1);
+by (fast_tac (claset() addEs  [inj_ontoD, f_eq_gE]) 1);
 qed "bij_if_then_else";
 
 goal Lfp.thy "? X. X = Compl(g``Compl((f:: 'a=>'b)``X))";