# HG changeset patch
# User paulson
# Date 838376715 -7200
# Node ID acb7363994cb0abf6d3c234e0348ee33b684f028
# Parent  e2946beeb9ff8c4b0c6ca5eb2c038242be8a9928
Removal of cfast_tac

diff -r e2946beeb9ff -r acb7363994cb src/HOL/ex/PropLog.ML
--- a/src/HOL/ex/PropLog.ML	Fri Jul 26 12:23:45 1996 +0200
+++ b/src/HOL/ex/PropLog.ML	Fri Jul 26 12:25:15 1996 +0200
@@ -207,9 +207,9 @@
 qed "completeness_0";
 
 (*A semantic analogue of the Deduction Theorem*)
-val [sat] = goalw PropLog.thy [sat_def] "insert p H |= q ==> H |= p->q";
+goalw PropLog.thy [sat_def] "!!p H. insert p H |= q ==> H |= p->q";
 by (Simp_tac 1);
-by (cfast_tac [sat] 1);
+by (Fast_tac 1);
 qed "sat_imp";
 
 val [finite] = goal PropLog.thy "H: Fin({p.True}) ==> !p. H |= p --> H |- p";
diff -r e2946beeb9ff -r acb7363994cb src/HOL/ex/Simult.ML
--- a/src/HOL/ex/Simult.ML	Fri Jul 26 12:23:45 1996 +0200
+++ b/src/HOL/ex/Simult.ML	Fri Jul 26 12:25:15 1996 +0200
@@ -55,10 +55,11 @@
 qed "TF_induct";
 
 (*This lemma replaces a use of subgoal_tac to prove tree_forest_induct*)
-val prems = goalw Simult.thy [Part_def]
- "! M: TF(A). (M: Part (TF A) In0 --> P(M)) & (M: Part (TF A) In1 --> Q(M)) \
-\ ==> (! M: Part (TF A) In0. P(M)) & (! M: Part (TF A) In1. Q(M))";
-by (cfast_tac prems 1);
+goalw Simult.thy [Part_def]
+ "!!A.  ! M: TF(A). (M: Part (TF A) In0 --> P(M)) & \
+\                   (M: Part (TF A) In1 --> Q(M)) \
+\  ==> (! M: Part (TF A) In0. P(M)) & (! M: Part (TF A) In1. Q(M))";
+by (Fast_tac 1);
 qed "TF_induct_lemma";
 
 AddSIs [PartI];
diff -r e2946beeb9ff -r acb7363994cb src/HOL/ex/set.ML
--- a/src/HOL/ex/set.ML	Fri Jul 26 12:23:45 1996 +0200
+++ b/src/HOL/ex/set.ML	Fri Jul 26 12:25:15 1996 +0200
@@ -50,8 +50,8 @@
 by (fast_tac (!claset addEs [Inv_f_f RS ssubst]) 1);
 qed "inv_image_comp";
 
-val prems = goal Set.thy "f(a) ~: (f``X) ==> a~:X";
-by (cfast_tac prems 1);
+goal Set.thy "!!f. f(a) ~: (f``X) ==> a~:X";
+by (Fast_tac 1);
 qed "contra_imageI";
 
 goal Lfp.thy "(a ~: Compl(X)) = (a:X)";
@@ -66,17 +66,10 @@
             rtac imageI, rtac Xa]);
 qed "disj_lemma";
 
-goal Lfp.thy "range(%z. if z:X then f(z) else g(z)) = f``X Un g``Compl(X)";
-by (rtac equalityI 1);
-by (rewtac range_def);
-by (fast_tac (!claset addIs [if_P RS sym, if_not_P RS sym]) 2);
-by (rtac subsetI 1);
-by (etac CollectE 1);
-by (etac exE 1);
-by (etac ssubst 1);
-by (rtac (excluded_middle RS disjE) 1);
-by (EVERY' [rtac (if_P     RS ssubst), atac, Fast_tac] 2);
-by (EVERY' [rtac (if_not_P RS ssubst), atac, Fast_tac] 1);
+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 setloop split_tac [expand_if]) 1);
+by (Fast_tac 1);
 qed "range_if_then_else";
 
 goal Lfp.thy "a : X Un Compl(X)";