Ran expandshort, especially to introduce Safe_tac
authorpaulson
Wed Nov 05 13:14:15 1997 +0100 (1997-11-05)
changeset 4152451104c223e2
parent 4151 5c19cd418c33
child 4153 e534c4c32d54
Ran expandshort, especially to introduce Safe_tac
src/ZF/AC/AC10_AC15.ML
src/ZF/AC/WO2_AC16.ML
src/ZF/AC/WO6_WO1.ML
src/ZF/AC/rel_is_fun.ML
src/ZF/Cardinal.ML
src/ZF/CardinalArith.ML
src/ZF/Coind/ECR.ML
src/ZF/Coind/MT.ML
src/ZF/Coind/Map.ML
src/ZF/EquivClass.ML
src/ZF/Finite.ML
src/ZF/IMP/Equiv.ML
src/ZF/Order.ML
src/ZF/OrderArith.ML
src/ZF/OrderType.ML
src/ZF/Ordinal.ML
src/ZF/Perm.ML
src/ZF/Resid/Confluence.ML
src/ZF/Resid/Cube.ML
src/ZF/Resid/Reduction.ML
src/ZF/Resid/Residuals.ML
src/ZF/Resid/SubUnion.ML
src/ZF/Univ.ML
src/ZF/Zorn.ML
src/ZF/ex/Integ.ML
src/ZF/ex/LList.ML
src/ZF/ex/Limit.ML
src/ZF/ex/Mutil.ML
src/ZF/ex/Ntree.ML
src/ZF/ex/Primes.ML
src/ZF/ex/Primrec.ML
src/ZF/ex/PropLog.ML
src/ZF/ex/Ramsey.ML
src/ZF/ex/Term.ML
src/ZF/ex/misc.ML
     1.1 --- a/src/ZF/AC/AC10_AC15.ML	Wed Nov 05 11:49:34 1997 +0100
     1.2 +++ b/src/ZF/AC/AC10_AC15.ML	Wed Nov 05 13:14:15 1997 +0100
     1.3 @@ -141,7 +141,7 @@
     1.4  (* ********************************************************************** *)
     1.5  
     1.6  goalw thy AC_defs "!!Z. AC12 ==> AC15";
     1.7 -by (safe_tac (claset()));
     1.8 +by Safe_tac;
     1.9  by (etac allE 1);
    1.10  by (etac impE 1);
    1.11  by (etac cons_times_nat_not_Finite 1);
    1.12 @@ -167,7 +167,7 @@
    1.13  (* ********************************************************************** *)
    1.14  
    1.15  goalw thy AC_defs "!!n. [| n:nat; 1 le n; AC10(n) |] ==> AC13(n)";
    1.16 -by (safe_tac (claset()));
    1.17 +by Safe_tac;
    1.18  by (fast_tac (empty_cs addSEs [allE, cons_times_nat_not_Finite RSN (2, impE),
    1.19                                  ex_fun_AC13_AC15]) 1);
    1.20  qed "AC10_AC13";
     2.1 --- a/src/ZF/AC/WO2_AC16.ML	Wed Nov 05 11:49:34 1997 +0100
     2.2 +++ b/src/ZF/AC/WO2_AC16.ML	Wed Nov 05 13:14:15 1997 +0100
     2.3 @@ -48,7 +48,7 @@
     2.4  \               ==> ALL y<x. ALL z<a. z < y | (EX Y:F(y). fa(z) <= Y) -->  \
     2.5  \                       (EX! Y. Y : F(y) & fa(z) <= Y)";
     2.6  by (REPEAT (resolve_tac [oallI, impI] 1));
     2.7 -by (dresolve_tac [ospec] 1 THEN (assume_tac 1));
     2.8 +by (dtac ospec 1 THEN (assume_tac 1));
     2.9  by (fast_tac (FOL_cs addSEs [oallE]) 1);
    2.10  val lemma4 = result();
    2.11  
    2.12 @@ -62,7 +62,7 @@
    2.13  by (rtac conjI 1);
    2.14  by (rtac subsetI 1);
    2.15  by (etac OUN_E 1);
    2.16 -by (dresolve_tac [ospec] 1 THEN (assume_tac 1));
    2.17 +by (dtac ospec 1 THEN (assume_tac 1));
    2.18  by (Fast_tac 1);
    2.19  by (dtac lemma4 1 THEN (assume_tac 1));
    2.20  by (rtac oallI 1);
    2.21 @@ -322,7 +322,7 @@
    2.22  goal thy "!!j. [| ALL y<succ(j). F(y)<=X & (ALL x<a. x<y | P(x,y)  \
    2.23  \       --> Q(x,y)); succ(j)<a |]  \
    2.24  \       ==> F(j)<=X & (ALL x<a. x<j | P(x,j) --> Q(x,j))";
    2.25 -by (dresolve_tac [ospec] 1);
    2.26 +by (dtac ospec 1);
    2.27  by (resolve_tac [lt_Ord RS (succI1 RS ltI RS lt_Ord RS le_refl)] 1
    2.28          THEN (REPEAT (assume_tac 1)));
    2.29  val lemma6 = result();
     3.1 --- a/src/ZF/AC/WO6_WO1.ML	Wed Nov 05 11:49:34 1997 +0100
     3.2 +++ b/src/ZF/AC/WO6_WO1.ML	Wed Nov 05 13:14:15 1997 +0100
     3.3 @@ -21,7 +21,7 @@
     3.4  qed "lt_oadd_odiff_disj";
     3.5  
     3.6  (*The corresponding elimination rule*)
     3.7 -val lt_oadd_odiff_cases = rule_by_tactic (safe_tac (claset()))
     3.8 +val lt_oadd_odiff_cases = rule_by_tactic Safe_tac
     3.9                                           (lt_oadd_odiff_disj RS disjE);
    3.10  
    3.11  (* ********************************************************************** *)
    3.12 @@ -353,7 +353,7 @@
    3.13  
    3.14  goal thy "EX y. x Un y*y <= y";
    3.15  by (res_inst_tac [("x","UN n:nat. rec(n, x, %k r. r Un r*r)")] exI 1);
    3.16 -by (safe_tac (claset()));
    3.17 +by Safe_tac;
    3.18  by (rtac (nat_0I RS UN_I) 1);
    3.19  by (Asm_simp_tac 1);
    3.20  by (res_inst_tac [("a","succ(n Un na)")] UN_I 1);
     4.1 --- a/src/ZF/AC/rel_is_fun.ML	Wed Nov 05 11:49:34 1997 +0100
     4.2 +++ b/src/ZF/AC/rel_is_fun.ML	Wed Nov 05 13:14:15 1997 +0100
     4.3 @@ -27,7 +27,7 @@
     4.4  goalw Cardinal.thy [function_def]
     4.5      "!!r. [| succ(m) lepoll domain(r); r lepoll succ(m); m:nat |] ==> \
     4.6  \         function(r)";
     4.7 -by (safe_tac (claset()));
     4.8 +by Safe_tac;
     4.9  by (resolve_tac [excluded_middle RS disjE] 1 THEN (atac 2));
    4.10  by (fast_tac (claset() addSEs [lepoll_trans RS succ_lepoll_natE, 
    4.11                          Diff_sing_lepoll RSN (2, lepoll_m_imp_domain_lepoll_m)]
     5.1 --- a/src/ZF/Cardinal.ML	Wed Nov 05 11:49:34 1997 +0100
     5.2 +++ b/src/ZF/Cardinal.ML	Wed Nov 05 13:14:15 1997 +0100
     5.3 @@ -239,7 +239,7 @@
     5.4  
     5.5  goal Cardinal.thy "Ord(LEAST x. P(x))";
     5.6  by (excluded_middle_tac "EX i. Ord(i) & P(i)" 1);
     5.7 -by (safe_tac (claset()));
     5.8 +by Safe_tac;
     5.9  by (rtac (Least_le RS ltE) 2);
    5.10  by (REPEAT_SOME assume_tac);
    5.11  by (etac (Least_0 RS ssubst) 1);
    5.12 @@ -351,7 +351,7 @@
    5.13  by (excluded_middle_tac "EX i. Ord(i) & i eqpoll A" 1);
    5.14  by (etac (Least_0 RS ssubst) 1 THEN rtac Card_0 1);
    5.15  by (rtac (Ord_Least RS CardI) 1);
    5.16 -by (safe_tac (claset()));
    5.17 +by Safe_tac;
    5.18  by (rtac less_LeastE 1);
    5.19  by (assume_tac 2);
    5.20  by (etac eqpoll_trans 1);
    5.21 @@ -433,7 +433,7 @@
    5.22  
    5.23  goalw Cardinal.thy [lepoll_def, inj_def]
    5.24   "!!A B. [| cons(u,A) lepoll cons(v,B);  u~:A;  v~:B |] ==> A lepoll B";
    5.25 -by (safe_tac (claset()));
    5.26 +by Safe_tac;
    5.27  by (res_inst_tac [("x", "lam x:A. if(f`x=v, f`u, f`x)")] exI 1);
    5.28  by (rtac CollectI 1);
    5.29  (*Proving it's in the function space A->B*)
    5.30 @@ -568,7 +568,7 @@
    5.31  (*Congruence law for  cons  under equipollence*)
    5.32  goalw Cardinal.thy [lepoll_def]
    5.33      "!!A B. [| A lepoll B;  b ~: B |] ==> cons(a,A) lepoll cons(b,B)";
    5.34 -by (safe_tac (claset()));
    5.35 +by Safe_tac;
    5.36  by (res_inst_tac [("x", "lam y: cons(a,A).if(y=a, b, f`y)")] exI 1);
    5.37  by (res_inst_tac [("d","%z. if(z:B, converse(f)`z, a)")] 
    5.38      lam_injective 1);
    5.39 @@ -650,7 +650,7 @@
    5.40  by (rtac cons_lepoll_consD 1);
    5.41  by (rtac mem_not_refl 3);
    5.42  by (eresolve_tac [cons_Diff RS ssubst] 1);
    5.43 -by (safe_tac (claset()));
    5.44 +by Safe_tac;
    5.45  qed "Diff_sing_lepoll";
    5.46  
    5.47  (*If A has at least n+1 elements then A-{a} has at least n.*)
     6.1 --- a/src/ZF/CardinalArith.ML	Wed Nov 05 11:49:34 1997 +0100
     6.2 +++ b/src/ZF/CardinalArith.ML	Wed Nov 05 13:14:15 1997 +0100
     6.3 @@ -140,7 +140,7 @@
     6.4  by (rtac exI 1);
     6.5  by (res_inst_tac [("c", "%<x,y>.<y,x>"), ("d", "%<x,y>.<y,x>")] 
     6.6      lam_bijective 1);
     6.7 -by (safe_tac (claset()));
     6.8 +by Safe_tac;
     6.9  by (ALLGOALS (Asm_simp_tac));
    6.10  qed "prod_commute_eqpoll";
    6.11  
    6.12 @@ -192,7 +192,7 @@
    6.13  goalw CardinalArith.thy [eqpoll_def] "0*A eqpoll 0";
    6.14  by (rtac exI 1);
    6.15  by (rtac lam_bijective 1);
    6.16 -by (safe_tac (claset()));
    6.17 +by Safe_tac;
    6.18  qed "prod_0_eqpoll";
    6.19  
    6.20  goalw CardinalArith.thy [cmult_def] "0 |*| i = 0";
    6.21 @@ -604,7 +604,7 @@
    6.22  by (rewtac Transset_def);
    6.23  by (safe_tac subset_cs);
    6.24  by (asm_full_simp_tac (simpset() addsimps [ordertype_pred_unfold]) 1);
    6.25 -by (safe_tac (claset()));
    6.26 +by Safe_tac;
    6.27  by (rtac UN_I 1);
    6.28  by (rtac ReplaceI 2);
    6.29  by (ALLGOALS (blast_tac (claset() addIs [well_ord_subset] addSEs [predE])));
     7.1 --- a/src/ZF/Coind/ECR.ML	Wed Nov 05 11:49:34 1997 +0100
     7.2 +++ b/src/ZF/Coind/ECR.ML	Wed Nov 05 13:14:15 1997 +0100
     7.3 @@ -49,7 +49,7 @@
     7.4  goalw ECR.thy [hastyenv_def]
     7.5    "!!ve.[| ve:ValEnv; te:TyEnv; hastyenv(ve,te); <v,t>:HasTyRel |] ==> \
     7.6  \   hastyenv(ve_owr(ve,x,v),te_owr(te,x,t))";
     7.7 -by (safe_tac (claset()));
     7.8 +by Safe_tac;
     7.9  by (stac ve_dom_owr 1);
    7.10  by (assume_tac 1);
    7.11  by (etac (HasTyRel.dom_subset RS subsetD RS SigmaD1 RS ValNEE) 1);
    7.12 @@ -69,10 +69,10 @@
    7.13  
    7.14  goalw ECR.thy  [isofenv_def,hastyenv_def]
    7.15    "!!ve.[| ve:ValEnv; te:TyEnv; isofenv(ve,te) |] ==> hastyenv(ve,te)";
    7.16 -by (safe_tac (claset()));
    7.17 +by Safe_tac;
    7.18  by (dtac bspec 1);
    7.19  by (assume_tac 1);
    7.20 -by (safe_tac (claset()));
    7.21 +by Safe_tac;
    7.22  by (dtac HasTyRel.htr_constI 1);
    7.23  by (assume_tac 2);
    7.24  by (etac te_appI 1);
     8.1 --- a/src/ZF/Coind/MT.ML	Wed Nov 05 11:49:34 1997 +0100
     8.2 +++ b/src/ZF/Coind/MT.ML	Wed Nov 05 13:14:15 1997 +0100
     8.3 @@ -51,7 +51,7 @@
     8.4  \  <cl,t>:HasTyRel";
     8.5  by (cut_facts_tac prems 1);
     8.6  by (etac elab_fixE 1);
     8.7 -by (safe_tac (claset()));
     8.8 +by Safe_tac;
     8.9  by (EVERY [forward_tac [subst] 1,atac 2,rtac htr_closCI 1]);
    8.10  by clean_tac;
    8.11  by (rtac ve_owrI 1);
    8.12 @@ -129,7 +129,7 @@
    8.13  by (etac htr_closE 1);
    8.14  by (etac elab_fnE 1);
    8.15  by (rewrite_tac Ty.con_defs);
    8.16 -by (safe_tac (claset()));
    8.17 +by Safe_tac;
    8.18  by (dtac (spec RS spec RS mp RS mp) 1);
    8.19  by (assume_tac 3);
    8.20  by (assume_tac 2);
     9.1 --- a/src/ZF/Coind/Map.ML	Wed Nov 05 11:49:34 1997 +0100
     9.2 +++ b/src/ZF/Coind/Map.ML	Wed Nov 05 13:14:15 1997 +0100
     9.3 @@ -69,7 +69,7 @@
     9.4  (** map_emp **)
     9.5  
     9.6  goalw Map.thy [map_emp_def,PMap_def,TMap_def] "map_emp:PMap(A,B)";
     9.7 -by (safe_tac (claset()));
     9.8 +by Safe_tac;
     9.9  by (rtac image_02 1);
    9.10  qed "pmap_empI";
    9.11  
    9.12 @@ -89,7 +89,7 @@
    9.13  by (dres_inst_tac [("psi", "?uu ~: B")] asm_rl 1);
    9.14  by (asm_full_simp_tac
    9.15      (simpset() addsimps [qbeta] setloop split_tac [expand_if]) 1);
    9.16 -by (safe_tac (claset()));
    9.17 +by Safe_tac;
    9.18  by (dres_inst_tac [("psi", "?uu ~: B")] asm_rl 3);
    9.19  by (ALLGOALS Asm_full_simp_tac);
    9.20  by (Fast_tac 1);
    10.1 --- a/src/ZF/EquivClass.ML	Wed Nov 05 11:49:34 1997 +0100
    10.2 +++ b/src/ZF/EquivClass.ML	Wed Nov 05 13:14:15 1997 +0100
    10.3 @@ -143,7 +143,7 @@
    10.4  \       !!x.  x : A ==> b(x) : B |]     \
    10.5  \    ==> (UN x:X. b(x)) : B";
    10.6  by (cut_facts_tac prems 1);
    10.7 -by (safe_tac (claset()));
    10.8 +by Safe_tac;
    10.9  by (asm_simp_tac (simpset() addsimps (UN_equiv_class::prems)) 1);
   10.10  qed "UN_equiv_class_type";
   10.11  
   10.12 @@ -156,7 +156,7 @@
   10.13  \       !!x y. [| x:A; y:A; b(x)=b(y) |] ==> <x,y>:r |]         \
   10.14  \    ==> X=Y";
   10.15  by (cut_facts_tac prems 1);
   10.16 -by (safe_tac (claset()));
   10.17 +by Safe_tac;
   10.18  by (rtac equiv_class_eq 1);
   10.19  by (REPEAT (ares_tac prems 1));
   10.20  by (etac box_equals 1);
   10.21 @@ -176,7 +176,7 @@
   10.22      "[| equiv(A,r);  congruent2(r,b);  a: A |] ==> \
   10.23  \    congruent(r, %x1. UN x2:r``{a}. b(x1,x2))";
   10.24  by (cut_facts_tac (equivA::prems) 1);
   10.25 -by (safe_tac (claset()));
   10.26 +by Safe_tac;
   10.27  by (rtac (equivA RS equiv_type RS subsetD RS SigmaE2) 1);
   10.28  by (assume_tac 1);
   10.29  by (asm_simp_tac (simpset() addsimps [equivA RS UN_equiv_class,
   10.30 @@ -201,7 +201,7 @@
   10.31  \       !!x1 x2.  [| x1: A; x2: A |] ==> b(x1,x2) : B   \
   10.32  \    |] ==> (UN x1:X1. UN x2:X2. b(x1,x2)) : B";
   10.33  by (cut_facts_tac prems 1);
   10.34 -by (safe_tac (claset()));
   10.35 +by Safe_tac;
   10.36  by (REPEAT (ares_tac (prems@[UN_equiv_class_type,
   10.37                               congruent2_implies_congruent_UN,
   10.38                               congruent2_implies_congruent, quotientI]) 1));
   10.39 @@ -216,7 +216,7 @@
   10.40  \       !! y z w. [| w: A;  <y,z> : r |] ==> b(w,y) = b(w,z)       \
   10.41  \    |] ==> congruent2(r,b)";
   10.42  by (cut_facts_tac prems 1);
   10.43 -by (safe_tac (claset()));
   10.44 +by Safe_tac;
   10.45  by (rtac trans 1);
   10.46  by (REPEAT (ares_tac prems 1
   10.47       ORELSE etac (subsetD RS SigmaE2) 1 THEN assume_tac 2 THEN assume_tac 1));
   10.48 @@ -244,7 +244,7 @@
   10.49  val congt' = rewrite_rule [congruent_def] congt;
   10.50  by (cut_facts_tac [ZinA] 1);
   10.51  by (rewtac congruent_def);
   10.52 -by (safe_tac (claset()));
   10.53 +by Safe_tac;
   10.54  by (rtac (equivA RS equiv_type RS subsetD RS SigmaE2) 1);
   10.55  by (assume_tac 1);
   10.56  by (asm_simp_tac (simpset() addsimps [commute,
    11.1 --- a/src/ZF/Finite.ML	Wed Nov 05 11:49:34 1997 +0100
    11.2 +++ b/src/ZF/Finite.ML	Wed Nov 05 13:14:15 1997 +0100
    11.3 @@ -60,7 +60,7 @@
    11.4  by (etac Fin_induct 1);
    11.5  by (simp_tac (simpset() addsimps [subset_empty_iff]) 1);
    11.6  by (asm_simp_tac (simpset() addsimps subset_cons_iff::distrib_simps) 1);
    11.7 -by (safe_tac (claset()));
    11.8 +by Safe_tac;
    11.9  by (eres_inst_tac [("b","z")] (cons_Diff RS subst) 1);
   11.10  by (Asm_simp_tac 1);
   11.11  qed "Fin_subset_lemma";
   11.12 @@ -131,7 +131,7 @@
   11.13  by (etac FiniteFun.induct 1);
   11.14  by (simp_tac (simpset() addsimps subset_empty_iff::FiniteFun.intrs) 1);
   11.15  by (asm_simp_tac (simpset() addsimps subset_cons_iff::distrib_simps) 1);
   11.16 -by (safe_tac (claset()));
   11.17 +by Safe_tac;
   11.18  by (eres_inst_tac [("b","z")] (cons_Diff RS subst) 1);
   11.19  by (dtac (spec RS mp) 1 THEN assume_tac 1);
   11.20  by (fast_tac (claset() addSIs FiniteFun.intrs) 1);
    12.1 --- a/src/ZF/IMP/Equiv.ML	Wed Nov 05 11:49:34 1997 +0100
    12.2 +++ b/src/ZF/IMP/Equiv.ML	Wed Nov 05 13:14:15 1997 +0100
    12.3 @@ -90,7 +90,7 @@
    12.4      "c : com ==> ALL x:C(c). <c,fst(x)> -c-> snd(x)";
    12.5  by (rtac (prem RS com.induct) 1);
    12.6  by (rewrite_tac C_rewrite_rules);
    12.7 -by (safe_tac (claset()));
    12.8 +by Safe_tac;
    12.9  by (ALLGOALS Asm_full_simp_tac);
   12.10  
   12.11  (* skip *)
   12.12 @@ -107,7 +107,7 @@
   12.13  (* while *)
   12.14  by (EVERY1 [forward_tac [Gamma_bnd_mono], etac induct, atac]);
   12.15  by (rewtac Gamma_def);  
   12.16 -by (safe_tac (claset()));
   12.17 +by Safe_tac;
   12.18  by (EVERY1 [dtac bspec, atac]);
   12.19  by (ALLGOALS Asm_full_simp_tac);
   12.20  
    13.1 --- a/src/ZF/Order.ML	Wed Nov 05 11:49:34 1997 +0100
    13.2 +++ b/src/ZF/Order.ML	Wed Nov 05 13:14:15 1997 +0100
    13.3 @@ -44,12 +44,12 @@
    13.4  
    13.5  goalw Order.thy [well_ord_def]
    13.6      "!!r. well_ord(A,r) ==> wf[A](r)";
    13.7 -by (safe_tac (claset()));
    13.8 +by Safe_tac;
    13.9  qed "well_ord_is_wf";
   13.10  
   13.11  goalw Order.thy [well_ord_def, tot_ord_def, part_ord_def]
   13.12      "!!r. well_ord(A,r) ==> trans[A](r)";
   13.13 -by (safe_tac (claset()));
   13.14 +by Safe_tac;
   13.15  qed "well_ord_is_trans_on";
   13.16  
   13.17  goalw Order.thy [well_ord_def, tot_ord_def]
   13.18 @@ -274,7 +274,7 @@
   13.19  goalw Order.thy [ord_iso_def, mono_map_def]
   13.20      "!!f g. [| f: mono_map(A,r,B,s);  g: mono_map(B,s,A,r);     \
   13.21  \              f O g = id(B);  g O f = id(A) |] ==> f: ord_iso(A,r,B,s)";
   13.22 -by (safe_tac (claset()));
   13.23 +by Safe_tac;
   13.24  by (REPEAT_FIRST (ares_tac [fg_imp_bijective]));
   13.25  by (Blast_tac 1);
   13.26  by (subgoal_tac "<g`(f`x), g`(f`y)> : r" 1);
   13.27 @@ -305,7 +305,7 @@
   13.28  goalw Order.thy [linear_def, ord_iso_def]
   13.29      "!!A B r. [| linear(B,s);  f: ord_iso(A,r,B,s) |] ==> linear(A,r)";
   13.30  by (Asm_simp_tac 1);
   13.31 -by (safe_tac (claset()));
   13.32 +by Safe_tac;
   13.33  by (dres_inst_tac [("x1", "f`x"), ("x", "f`xa")] (bspec RS bspec) 1);
   13.34  by (safe_tac (claset() addSEs [bij_is_fun RS apply_type]));
   13.35  by (dres_inst_tac [("t", "op `(converse(f))")] subst_context 1);
   13.36 @@ -316,7 +316,7 @@
   13.37      "!!A B r. [| wf[B](s);  f: ord_iso(A,r,B,s) |] ==> wf[A](r)";
   13.38  (*reversed &-congruence rule handles context of membership in A*)
   13.39  by (asm_full_simp_tac (simpset() addcongs [conj_cong2]) 1);
   13.40 -by (safe_tac (claset()));
   13.41 +by Safe_tac;
   13.42  by (dres_inst_tac [("x", "{f`z. z:Z Int A}")] spec 1);
   13.43  by (safe_tac (claset() addSIs [equalityI]));
   13.44  by (ALLGOALS (blast_tac
   13.45 @@ -430,7 +430,7 @@
   13.46  by (forward_tac [well_ord_iso_subset_lemma] 1);
   13.47  by (res_inst_tac [("f","converse(f)"), ("g","g")] ord_iso_trans 1);
   13.48  by (REPEAT_FIRST (ares_tac [subset_refl, ord_iso_sym]));
   13.49 -by (safe_tac (claset()));
   13.50 +by Safe_tac;
   13.51  by (forward_tac [ord_iso_converse] 1);
   13.52  by (EVERY (map (blast_tac bij_apply_cs) [1,1,1]));
   13.53  by (asm_full_simp_tac bij_inverse_ss 1);
   13.54 @@ -489,7 +489,7 @@
   13.55  \          : mono_map(domain(ord_iso_map(A,r,B,s)), r,  \
   13.56  \                     range(ord_iso_map(A,r,B,s)), s)";
   13.57  by (asm_simp_tac (simpset() addsimps [ord_iso_map_fun]) 1);
   13.58 -by (safe_tac (claset()));
   13.59 +by Safe_tac;
   13.60  by (subgoals_tac ["x:A", "xa:A", "y:B", "ya:B"] 1);
   13.61  by (REPEAT 
   13.62      (blast_tac (claset() addSEs [ord_iso_map_subset RS subsetD RS SigmaE]) 2));
    14.1 --- a/src/ZF/OrderArith.ML	Wed Nov 05 11:49:34 1997 +0100
    14.2 +++ b/src/ZF/OrderArith.ML	Wed Nov 05 13:14:15 1997 +0100
    14.3 @@ -125,7 +125,7 @@
    14.4  by (safe_tac (claset() addSIs [sum_bij]));
    14.5  (*Do the beta-reductions now*)
    14.6  by (ALLGOALS (Asm_full_simp_tac));
    14.7 -by (safe_tac (claset()));
    14.8 +by Safe_tac;
    14.9  (*8 subgoals!*)
   14.10  by (ALLGOALS
   14.11      (asm_full_simp_tac 
   14.12 @@ -141,7 +141,7 @@
   14.13      lam_bijective 1);
   14.14  by (blast_tac (claset() addSIs [if_type]) 2);
   14.15  by (DEPTH_SOLVE_1 (eresolve_tac [case_type, UnI1, UnI2] 1));
   14.16 -by (safe_tac (claset()));
   14.17 +by Safe_tac;
   14.18  by (ALLGOALS (asm_simp_tac (simpset() setloop split_tac [expand_if])));
   14.19  by (blast_tac (claset() addEs [equalityE]) 1);
   14.20  qed "sum_disjoint_bij";
   14.21 @@ -249,7 +249,7 @@
   14.22  \        (lam <x,y>:A*B. <f`x, g`y>) : bij(A*B, C*D)";
   14.23  by (res_inst_tac [("d", "%<x,y>. <converse(f)`x, converse(g)`y>")] 
   14.24      lam_bijective 1);
   14.25 -by (safe_tac (claset()));
   14.26 +by Safe_tac;
   14.27  by (ALLGOALS (asm_simp_tac bij_inverse_ss));
   14.28  qed "prod_bij";
   14.29  
   14.30 @@ -266,7 +266,7 @@
   14.31  
   14.32  goal OrderArith.thy "(lam z:A. <x,z>) : bij(A, {x}*A)";
   14.33  by (res_inst_tac [("d", "snd")] lam_bijective 1);
   14.34 -by (safe_tac (claset()));
   14.35 +by Safe_tac;
   14.36  by (ALLGOALS Asm_simp_tac);
   14.37  qed "singleton_prod_bij";
   14.38  
    15.1 --- a/src/ZF/OrderType.ML	Wed Nov 05 11:49:34 1997 +0100
    15.2 +++ b/src/ZF/OrderType.ML	Wed Nov 05 13:14:15 1997 +0100
    15.3 @@ -103,13 +103,13 @@
    15.4  
    15.5  goalw OrderType.thy [well_ord_def, tot_ord_def, part_ord_def]
    15.6      "!!r. [| well_ord(A,r);  x:A |] ==> Ord(ordermap(A,r) ` x)";
    15.7 -by (safe_tac (claset()));
    15.8 +by Safe_tac;
    15.9  by (wf_on_ind_tac "x" [] 1);
   15.10  by (asm_simp_tac (simpset() addsimps [ordermap_pred_unfold]) 1);
   15.11  by (rtac (Ord_is_Transset RSN (2,OrdI)) 1);
   15.12  by (rewrite_goals_tac [pred_def,Transset_def]);
   15.13  by (Blast_tac 2);
   15.14 -by (safe_tac (claset()));
   15.15 +by Safe_tac;
   15.16  by (ordermap_elim_tac 1);
   15.17  by (fast_tac (claset() addSEs [trans_onD]) 1);
   15.18  qed "Ord_ordermap";
   15.19 @@ -120,7 +120,7 @@
   15.20  by (rtac (Ord_is_Transset RSN (2,OrdI)) 1);
   15.21  by (blast_tac (claset() addIs [Ord_ordermap]) 2);
   15.22  by (rewrite_goals_tac [Transset_def,well_ord_def]);
   15.23 -by (safe_tac (claset()));
   15.24 +by Safe_tac;
   15.25  by (ordermap_elim_tac 1);
   15.26  by (Blast_tac 1);
   15.27  qed "Ord_ordertype";
   15.28 @@ -139,7 +139,7 @@
   15.29  goalw OrderType.thy [well_ord_def, tot_ord_def]
   15.30      "!!r. [| ordermap(A,r)`w : ordermap(A,r)`x;  well_ord(A,r);  \
   15.31  \            w: A; x: A |] ==> <w,x>: r";
   15.32 -by (safe_tac (claset()));
   15.33 +by Safe_tac;
   15.34  by (linear_case_tac 1);
   15.35  by (blast_tac (claset() addSEs [mem_not_refl RS notE]) 1);
   15.36  by (dtac ordermap_mono 1);
   15.37 @@ -312,7 +312,7 @@
   15.38  
   15.39  goal OrderType.thy "(lam z:A+0. case(%x. x, %y. y, z)) : bij(A+0, A)";
   15.40  by (res_inst_tac [("d", "Inl")] lam_bijective 1);
   15.41 -by (safe_tac (claset()));
   15.42 +by Safe_tac;
   15.43  by (ALLGOALS Asm_simp_tac);
   15.44  qed "bij_sum_0";
   15.45  
   15.46 @@ -325,7 +325,7 @@
   15.47  
   15.48  goal OrderType.thy "(lam z:0+A. case(%x. x, %y. y, z)) : bij(0+A, A)";
   15.49  by (res_inst_tac [("d", "Inr")] lam_bijective 1);
   15.50 -by (safe_tac (claset()));
   15.51 +by Safe_tac;
   15.52  by (ALLGOALS Asm_simp_tac);
   15.53  qed "bij_0_sum";
   15.54  
   15.55 @@ -344,7 +344,7 @@
   15.56  \        (lam x:pred(A,a,r). Inl(x))    \
   15.57  \        : bij(pred(A,a,r), pred(A+B, Inl(a), radd(A,r,B,s)))";
   15.58  by (res_inst_tac [("d", "case(%x. x, %y. y)")] lam_bijective 1);
   15.59 -by (safe_tac (claset()));
   15.60 +by Safe_tac;
   15.61  by (ALLGOALS
   15.62      (asm_full_simp_tac 
   15.63       (simpset() addsimps [radd_Inl_iff, radd_Inr_Inl_iff])));
   15.64 @@ -364,7 +364,7 @@
   15.65  \        id(A+pred(B,b,s))      \
   15.66  \        : bij(A+pred(B,b,s), pred(A+B, Inr(b), radd(A,r,B,s)))";
   15.67  by (res_inst_tac [("d", "%z. z")] lam_bijective 1);
   15.68 -by (safe_tac (claset()));
   15.69 +by Safe_tac;
   15.70  by (ALLGOALS (Asm_full_simp_tac));
   15.71  qed "pred_Inr_bij";
   15.72  
   15.73 @@ -671,7 +671,7 @@
   15.74  \        pred(A*B, <a,b>, rmult(A,r,B,s)) =     \
   15.75  \        pred(A,a,r)*B Un ({a} * pred(B,b,s))";
   15.76  by (rtac equalityI 1);
   15.77 -by (safe_tac (claset()));
   15.78 +by Safe_tac;
   15.79  by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [rmult_iff])));
   15.80  by (ALLGOALS (Blast_tac));
   15.81  qed "pred_Pair_eq";
   15.82 @@ -703,7 +703,7 @@
   15.83  by (REPEAT_FIRST (ares_tac [well_ord_rmult, well_ord_radd, well_ord_Memrel, 
   15.84                              Ord_ordertype]));
   15.85  by (ALLGOALS (asm_simp_tac (simpset() addsimps [Memrel_iff])));
   15.86 -by (safe_tac (claset()));
   15.87 +by Safe_tac;
   15.88  by (ALLGOALS (blast_tac (claset() addIs [Ord_trans])));
   15.89  qed "ordertype_pred_Pair_lemma";
   15.90  
    16.1 --- a/src/ZF/Ordinal.ML	Wed Nov 05 11:49:34 1997 +0100
    16.2 +++ b/src/ZF/Ordinal.ML	Wed Nov 05 13:14:15 1997 +0100
    16.3 @@ -183,7 +183,7 @@
    16.4  by (swap_res_tac [Ord_is_Transset RSN (2,OrdI)] 1);
    16.5  by (Blast_tac 2);
    16.6  by (rewtac Transset_def);
    16.7 -by (safe_tac (claset()));
    16.8 +by Safe_tac;
    16.9  by (Asm_full_simp_tac 1);
   16.10  by (REPEAT (eresolve_tac [asm_rl, Ord_in_Ord] 1));
   16.11  qed "ON_class";
    17.1 --- a/src/ZF/Perm.ML	Wed Nov 05 11:49:34 1997 +0100
    17.2 +++ b/src/ZF/Perm.ML	Wed Nov 05 13:14:15 1997 +0100
    17.3 @@ -44,7 +44,7 @@
    17.4  
    17.5  (*Cantor's theorem revisited*)
    17.6  goalw Perm.thy [surj_def] "f ~: surj(A,Pow(A))";
    17.7 -by (safe_tac (claset()));
    17.8 +by Safe_tac;
    17.9  by (cut_facts_tac [cantor] 1);
   17.10  by (fast_tac subset_cs 1);
   17.11  qed "cantor_surj";
   17.12 @@ -363,18 +363,18 @@
   17.13  
   17.14  goalw Perm.thy [inj_def]
   17.15      "!!f g. [| (f O g): inj(A,C);  g: A->B;  f: B->C |] ==> g: inj(A,B)";
   17.16 -by (safe_tac (claset()));
   17.17 +by Safe_tac;
   17.18  by (REPEAT (eresolve_tac [asm_rl, bspec RS bspec RS mp] 1));
   17.19  by (asm_simp_tac (simpset() ) 1);
   17.20  qed "comp_mem_injD1";
   17.21  
   17.22  goalw Perm.thy [inj_def,surj_def]
   17.23      "!!f g. [| (f O g): inj(A,C);  g: surj(A,B);  f: B->C |] ==> f: inj(B,C)";
   17.24 -by (safe_tac (claset()));
   17.25 +by Safe_tac;
   17.26  by (res_inst_tac [("x1", "x")] (bspec RS bexE) 1);
   17.27  by (eres_inst_tac [("x1", "w")] (bspec RS bexE) 3);
   17.28  by (REPEAT (assume_tac 1));
   17.29 -by (safe_tac (claset()));
   17.30 +by Safe_tac;
   17.31  by (res_inst_tac [("t", "op `(g)")] subst_context 1);
   17.32  by (REPEAT (eresolve_tac [asm_rl, bspec RS bspec RS mp] 1));
   17.33  by (asm_simp_tac (simpset() ) 1);
   17.34 @@ -392,7 +392,7 @@
   17.35  
   17.36  goalw Perm.thy [inj_def,surj_def]
   17.37      "!!f g. [| (f O g): surj(A,C);  g: A->B;  f: inj(B,C) |] ==> g: surj(A,B)";
   17.38 -by (safe_tac (claset()));
   17.39 +by Safe_tac;
   17.40  by (eres_inst_tac [("x1", "f`y")] (bspec RS bexE) 1);
   17.41  by (REPEAT (ares_tac [apply_type] 1 ORELSE dtac comp_fun_applyD 1));
   17.42  by (blast_tac (claset() addSIs [apply_funtype]) 1);
   17.43 @@ -426,7 +426,7 @@
   17.44  goalw Perm.thy [id_def]
   17.45      "!!f A B. [| f: A->B;  g: B->A |] ==> \
   17.46  \             f O g = id(B) <-> (ALL y:B. f`(g`y)=y)";
   17.47 -by (safe_tac (claset()));
   17.48 +by Safe_tac;
   17.49  by (dres_inst_tac [("t", "%h. h`y ")] subst_context 1);
   17.50  by (Asm_full_simp_tac 1);
   17.51  by (rtac fun_extension 1);
    18.1 --- a/src/ZF/Resid/Confluence.ML	Wed Nov 05 11:49:34 1997 +0100
    18.2 +++ b/src/ZF/Resid/Confluence.ML	Wed Nov 05 13:14:15 1997 +0100
    18.3 @@ -53,7 +53,7 @@
    18.4  
    18.5  goalw Confluence.thy [confluence_def] 
    18.6      "!!u.[|confluence(Spar_red)|]==> confluence(Sred)";
    18.7 -by(blast_tac (claset() addIs [par_red_red, red_par_red]) 1);
    18.8 +by (blast_tac (claset() addIs [par_red_red, red_par_red]) 1);
    18.9  val lemma1 = result();
   18.10  
   18.11  bind_thm ("confluence_beta_reduction",
    19.1 --- a/src/ZF/Resid/Cube.ML	Wed Nov 05 11:49:34 1997 +0100
    19.2 +++ b/src/ZF/Resid/Cube.ML	Wed Nov 05 13:14:15 1997 +0100
    19.3 @@ -34,7 +34,7 @@
    19.4  goal Cube.thy 
    19.5      "!!u.[|v <== u; regular(u); w~v|]==> \
    19.6  \       w |> u = (w|>v) |> (u|>v)";
    19.7 -by (resolve_tac [prism_l] 1);
    19.8 +by (rtac prism_l 1);
    19.9  by (rtac comp_trans 4);
   19.10  by (assume_tac 4);
   19.11  by (ALLGOALS(asm_simp_tac prism_ss));
   19.12 @@ -48,9 +48,9 @@
   19.13  goal Cube.thy 
   19.14      "!!u.[|u~v; regular(v); regular(u); w~u|]==>  \
   19.15  \          (w|>u) |> (v|>u) = (w|>v) |> (u|>v)";
   19.16 -by (rtac (preservation RS ssubst) 1 
   19.17 +by (stac preservation 1 
   19.18      THEN assume_tac 1 THEN assume_tac 1);
   19.19 -by (rtac (preservation RS ssubst) 1 
   19.20 +by (stac preservation 1 
   19.21      THEN etac comp_sym 1 THEN assume_tac 1);
   19.22  by (stac (prism RS sym) 1);
   19.23  by (asm_full_simp_tac (simpset() addsimps 
    20.1 --- a/src/ZF/Resid/Reduction.ML	Wed Nov 05 11:49:34 1997 +0100
    20.2 +++ b/src/ZF/Resid/Reduction.ML	Wed Nov 05 13:14:15 1997 +0100
    20.3 @@ -31,7 +31,7 @@
    20.4  	  [Spar_red.one_step, substL_type, redD1, redD2, par_redD1, 
    20.5  	   par_redD2, par_red1D2, unmark_type]);
    20.6  
    20.7 -val reducL_ss = simpset() setloop (SELECT_GOAL (safe_tac (claset())));
    20.8 +val reducL_ss = simpset() setloop (SELECT_GOAL Safe_tac);
    20.9  
   20.10  (* ------------------------------------------------------------------------- *)
   20.11  (*     Lemmas for reduction                                                  *)
    21.1 --- a/src/ZF/Resid/Residuals.ML	Wed Nov 05 11:49:34 1997 +0100
    21.2 +++ b/src/ZF/Resid/Residuals.ML	Wed Nov 05 13:14:15 1997 +0100
    21.3 @@ -100,11 +100,11 @@
    21.4  by (etac Scomp.induct 1);
    21.5  by (ALLGOALS (asm_full_simp_tac 
    21.6               (simpset() addsimps [res_Var,res_Fun,res_App,res_redex] 
    21.7 -              setloop (SELECT_GOAL (safe_tac (claset()))))));
    21.8 +              setloop (SELECT_GOAL Safe_tac))));
    21.9  by (dres_inst_tac [("psi", "Fun(?u) |> ?v : redexes")] asm_rl 1);
   21.10  by (asm_full_simp_tac 
   21.11               (simpset() addsimps [res_Fun] 
   21.12 -              setloop (SELECT_GOAL (safe_tac (claset())))) 1);
   21.13 +              setloop (SELECT_GOAL Safe_tac)) 1);
   21.14  qed "resfunc_type";
   21.15  
   21.16  Addsimps ([res_Var, res_Fun, res_App, res_redex, lift_rec_preserve_comp,
   21.17 @@ -112,7 +112,7 @@
   21.18  	  subst_rec_preserve_reg] @
   21.19  	  redexes.free_iffs);
   21.20  
   21.21 -val res1L_ss = simpset() setloop (SELECT_GOAL (safe_tac (claset())));
   21.22 +val res1L_ss = simpset() setloop (SELECT_GOAL Safe_tac);
   21.23  
   21.24  (* ------------------------------------------------------------------------- *)
   21.25  (*     Commutation theorem                                                   *)
   21.26 @@ -178,7 +178,7 @@
   21.27  goal Residuals.thy 
   21.28      "!!u. u~v ==> regular(u) --> regular(v) --> regular(u|>v)";
   21.29  by (etac Scomp.induct 1);
   21.30 -by (safe_tac (claset()));
   21.31 +by Safe_tac;
   21.32  by (TRYALL (dres_inst_tac [("psi", "regular(Fun(?u) |> ?v)")] asm_rl));
   21.33  by (ALLGOALS (asm_full_simp_tac res1L_ss));
   21.34  qed "residuals_preserve_reg";
   21.35 @@ -196,7 +196,7 @@
   21.36  goal Residuals.thy 
   21.37      "!!u. u ~ v ==> regular(v) --> u|>v = (u un v)|>v";
   21.38  by (etac Scomp.induct 1);
   21.39 -by (safe_tac (claset()));
   21.40 +by Safe_tac;
   21.41  by (dres_inst_tac [("psi", "Fun(?u) |> ?v = ?w")] asm_rl 3);
   21.42  by (ALLGOALS (asm_full_simp_tac (res1L_ss addsimps 
   21.43                                   [union_preserve_comp,comp_sym_iff])));
    22.1 --- a/src/ZF/Resid/SubUnion.ML	Wed Nov 05 11:49:34 1997 +0100
    22.2 +++ b/src/ZF/Resid/SubUnion.ML	Wed Nov 05 13:14:15 1997 +0100
    22.3 @@ -120,7 +120,7 @@
    22.4      "!!u. u ~ v ==> regular(u)-->regular(v)-->regular(u un v)";
    22.5  by (etac Scomp.induct 1);
    22.6  by (ALLGOALS(asm_full_simp_tac
    22.7 -             (simpset() setloop(SELECT_GOAL (safe_tac (claset()))))));
    22.8 +             (simpset() setloop(SELECT_GOAL Safe_tac))));
    22.9  by (dres_inst_tac [("psi", "regular(Fun(?u) un ?v)")] asm_rl 1);
   22.10  by (Asm_full_simp_tac 1);
   22.11  qed_spec_mp "union_preserve_regular";
    23.1 --- a/src/ZF/Univ.ML	Wed Nov 05 11:49:34 1997 +0100
    23.2 +++ b/src/ZF/Univ.ML	Wed Nov 05 13:14:15 1997 +0100
    23.3 @@ -93,13 +93,13 @@
    23.4  
    23.5  goal Univ.thy "!!a. a: Vfrom(A,i) ==> {a} : Vfrom(A,succ(i))";
    23.6  by (rtac subset_mem_Vfrom 1);
    23.7 -by (safe_tac (claset()));
    23.8 +by Safe_tac;
    23.9  qed "singleton_in_Vfrom";
   23.10  
   23.11  goal Univ.thy
   23.12      "!!A. [| a: Vfrom(A,i);  b: Vfrom(A,i) |] ==> {a,b} : Vfrom(A,succ(i))";
   23.13  by (rtac subset_mem_Vfrom 1);
   23.14 -by (safe_tac (claset()));
   23.15 +by Safe_tac;
   23.16  qed "doubleton_in_Vfrom";
   23.17  
   23.18  goalw Univ.thy [Pair_def]
   23.19 @@ -412,7 +412,7 @@
   23.20  val [ordi] = goal Univ.thy "Ord(i) ==> ALL b. b : Vset(i) --> rank(b) < i";
   23.21  by (rtac (ordi RS trans_induct) 1);
   23.22  by (stac Vset 1);
   23.23 -by (safe_tac (claset()));
   23.24 +by Safe_tac;
   23.25  by (stac rank 1);
   23.26  by (rtac UN_succ_least_lt 1);
   23.27  by (Blast_tac 2);
   23.28 @@ -445,7 +445,7 @@
   23.29  goal Univ.thy "!!i. Ord(i) ==> rank(Vset(i)) = i";
   23.30  by (stac rank 1);
   23.31  by (rtac equalityI 1);
   23.32 -by (safe_tac (claset()));
   23.33 +by Safe_tac;
   23.34  by (EVERY' [rtac UN_I, 
   23.35              etac (i_subset_Vfrom RS subsetD),
   23.36              etac (Ord_in_Ord RS rank_of_Ord RS ssubst),
   23.37 @@ -633,7 +633,7 @@
   23.38     "!!i. [| b: Fin(Vfrom(A,i));  Limit(i) |] ==> EX j. b <= Vfrom(A,j) & j<i";
   23.39  by (etac Fin_induct 1);
   23.40  by (blast_tac (claset() addSDs [Limit_has_0]) 1);
   23.41 -by (safe_tac (claset()));
   23.42 +by Safe_tac;
   23.43  by (etac Limit_VfromE 1);
   23.44  by (assume_tac 1);
   23.45  by (blast_tac (claset() addSIs [Un_least_lt] addIs [Vfrom_UnI1, Vfrom_UnI2]) 1);
   23.46 @@ -642,7 +642,7 @@
   23.47  goal Univ.thy "!!i. Limit(i) ==> Fin(Vfrom(A,i)) <= Vfrom(A,i)";
   23.48  by (rtac subsetI 1);
   23.49  by (dtac Fin_Vfrom_lemma 1);
   23.50 -by (safe_tac (claset()));
   23.51 +by Safe_tac;
   23.52  by (resolve_tac [Vfrom RS ssubst] 1);
   23.53  by (blast_tac (claset() addSDs [ltD]) 1);
   23.54  val Fin_VLimit = result();
    24.1 --- a/src/ZF/Zorn.ML	Wed Nov 05 11:49:34 1997 +0100
    24.2 +++ b/src/ZF/Zorn.ML	Wed Nov 05 13:14:15 1997 +0100
    24.3 @@ -206,7 +206,7 @@
    24.4  (*Now, verify that it increases*)
    24.5  by (asm_simp_tac (simpset() addsimps [Pow_iff, subset_refl]
    24.6                          setloop split_tac [expand_if]) 1);
    24.7 -by (safe_tac (claset()));
    24.8 +by Safe_tac;
    24.9  by (dtac choice_super 1);
   24.10  by (REPEAT (assume_tac 1));
   24.11  by (rewtac super_def);
   24.12 @@ -228,7 +228,7 @@
   24.13             setloop split_tac [expand_if]) 1);
   24.14  by (rewtac chain_def);
   24.15  by (rtac CollectI 1 THEN Blast_tac 1);
   24.16 -by (safe_tac(claset()));
   24.17 +by Safe_tac;
   24.18  by (res_inst_tac  [("m1","B"), ("n1","Ba")] (TFin_subset_linear RS disjE) 1);
   24.19  by (ALLGOALS Fast_tac);
   24.20  qed "TFin_chain_lemma4";
   24.21 @@ -272,13 +272,13 @@
   24.22  by (rename_tac "c" 1);
   24.23  by (res_inst_tac [("x", "Union(c)")] bexI 1);
   24.24  by (Blast_tac 2);
   24.25 -by (safe_tac (claset()));
   24.26 +by Safe_tac;
   24.27  by (rename_tac "z" 1);
   24.28  by (rtac classical 1);
   24.29  by (subgoal_tac "cons(z,c): super(S,c)" 1);
   24.30  by (blast_tac (claset() addEs [equalityE]) 1);
   24.31  by (rewtac super_def);
   24.32 -by (safe_tac (claset()));
   24.33 +by Safe_tac;
   24.34  by (fast_tac (claset() addEs [chain_extend]) 1);
   24.35  by (blast_tac (claset() addEs [equalityE]) 1);
   24.36  qed "Zorn";
    25.1 --- a/src/ZF/ex/Integ.ML	Wed Nov 05 11:49:34 1997 +0100
    25.2 +++ b/src/ZF/ex/Integ.ML	Wed Nov 05 13:14:15 1997 +0100
    25.3 @@ -94,7 +94,7 @@
    25.4  
    25.5  goalw Integ.thy [congruent_def]
    25.6      "congruent(intrel, %<x,y>. intrel``{<y,x>})";
    25.7 -by (safe_tac (claset()));
    25.8 +by Safe_tac;
    25.9  by (asm_full_simp_tac (simpset() addsimps add_ac) 1);
   25.10  qed "zminus_congruent";
   25.11  
   25.12 @@ -110,7 +110,7 @@
   25.13  goalw Integ.thy [integ_def,zminus_def]
   25.14      "!!z w. [| $~z = $~w;  z: integ;  w: integ |] ==> z=w";
   25.15  by (etac (zminus_ize UN_equiv_class_inject) 1);
   25.16 -by (safe_tac (claset()));
   25.17 +by Safe_tac;
   25.18  (*The setloop is only needed because assumptions are in the wrong order!*)
   25.19  by (asm_full_simp_tac (simpset() addsimps add_ac
   25.20                         setloop dtac eq_intrelD) 1);
   25.21 @@ -135,7 +135,7 @@
   25.22  
   25.23  (*No natural number is negative!*)
   25.24  goalw Integ.thy [znegative_def, znat_def]  "~ znegative($# n)";
   25.25 -by (safe_tac (claset()));
   25.26 +by Safe_tac;
   25.27  by (dres_inst_tac [("psi", "?lhs=?rhs")] asm_rl 1);
   25.28  by (dres_inst_tac [("psi", "?lhs<?rhs")] asm_rl 1);
   25.29  by (fast_tac (claset() addss
   25.30 @@ -155,7 +155,7 @@
   25.31  
   25.32  goalw Integ.thy [congruent_def]
   25.33      "congruent(intrel, %<x,y>. (y#-x) #+ (x#-y))";
   25.34 -by (safe_tac (claset()));
   25.35 +by Safe_tac;
   25.36  by (ALLGOALS Asm_simp_tac);
   25.37  by (etac rev_mp 1);
   25.38  by (res_inst_tac [("m","x1"),("n","y1")] diff_induct 1 THEN 
   25.39 @@ -209,7 +209,7 @@
   25.40  \         let <x1,y1>=z1; <x2,y2>=z2                 \
   25.41  \                           in intrel``{<x1#+x2, y1#+y2>})";
   25.42  (*Proof via congruent2_commuteI seems longer*)
   25.43 -by (safe_tac (claset()));
   25.44 +by Safe_tac;
   25.45  by (asm_simp_tac (simpset() addsimps [add_assoc, Let_def]) 1);
   25.46  (*The rest should be trivial, but rearranging terms is hard;
   25.47    add_ac does not help rewriting with the assumptions.*)
   25.48 @@ -305,7 +305,7 @@
   25.49  \               split(%x1 y1. split(%x2 y2.     \
   25.50  \                   intrel``{<x1#*x2 #+ y1#*y2, x1#*y2 #+ y1#*x2>}, p2), p1))";
   25.51  by (rtac (equiv_intrel RS congruent2_commuteI) 1);
   25.52 -by (safe_tac (claset()));
   25.53 +by Safe_tac;
   25.54  by (ALLGOALS Asm_simp_tac);
   25.55  (*Proof that zmult is congruent in one argument*)
   25.56  by (asm_simp_tac 
    26.1 --- a/src/ZF/ex/LList.ML	Wed Nov 05 11:49:34 1997 +0100
    26.2 +++ b/src/ZF/ex/LList.ML	Wed Nov 05 13:14:15 1997 +0100
    26.3 @@ -77,7 +77,7 @@
    26.4  by (REPEAT (resolve_tac [allI, impI] 1));
    26.5  by (etac lleq.elim 1);
    26.6  by (rewrite_goals_tac (QInr_def::llist.con_defs));
    26.7 -by (safe_tac (claset()));
    26.8 +by Safe_tac;
    26.9  by (fast_tac (subset_cs addSEs [Ord_trans, make_elim bspec]) 1);
   26.10  qed "lleq_Int_Vset_subset_lemma";
   26.11  
   26.12 @@ -89,7 +89,7 @@
   26.13  val [prem] = goal LList.thy "<l,l'> : lleq(A) ==> <l',l> : lleq(A)";
   26.14  by (rtac (prem RS converseI RS lleq.coinduct) 1);
   26.15  by (rtac (lleq.dom_subset RS converse_type) 1);
   26.16 -by (safe_tac (claset()));
   26.17 +by Safe_tac;
   26.18  by (etac lleq.elim 1);
   26.19  by (ALLGOALS Fast_tac);
   26.20  qed "lleq_symmetric";
   26.21 @@ -104,7 +104,7 @@
   26.22      "[| l=l';  l: llist(A) |] ==> <l,l'> : lleq(A)";
   26.23  by (res_inst_tac [("X", "{<l,l>. l: llist(A)}")] lleq.coinduct 1);
   26.24  by (rtac (lprem RS RepFunI RS (eqprem RS subst)) 1);
   26.25 -by (safe_tac (claset()));
   26.26 +by Safe_tac;
   26.27  by (etac llist.elim 1);
   26.28  by (ALLGOALS Fast_tac);
   26.29  qed "equal_llist_implies_leq";
    27.1 --- a/src/ZF/ex/Limit.ML	Wed Nov 05 11:49:34 1997 +0100
    27.2 +++ b/src/ZF/ex/Limit.ML	Wed Nov 05 13:14:15 1997 +0100
    27.3 @@ -13,7 +13,7 @@
    27.4  (* Useful goal commands.                                                *)
    27.5  (*----------------------------------------------------------------------*)
    27.6  
    27.7 -val brr = fn thl => fn n => by(REPEAT(ares_tac thl n));
    27.8 +val brr = fn thl => fn n => by (REPEAT(ares_tac thl n));
    27.9  val trr = fn thl => fn n => (REPEAT(ares_tac thl n));
   27.10  fun rotate n i = EVERY(replicate n (etac revcut_rl i));    
   27.11  
   27.12 @@ -70,7 +70,7 @@
   27.13  \                rel(D,x,z);  \
   27.14  \       !!x y. [| rel(D,x,y); rel(D,y,x); x:set(D); y:set(D)|] ==> x=y |] ==> \
   27.15  \    po(D)";
   27.16 -by (safe_tac (claset()));
   27.17 +by Safe_tac;
   27.18  brr prems 1;
   27.19  qed "poI";
   27.20  
   27.21 @@ -139,19 +139,19 @@
   27.22  
   27.23  val prems = goalw Limit.thy [islub_def]  (* islubI *)
   27.24      "[|isub(D,X,x); !!y. isub(D,X,y) ==> rel(D,x,y)|] ==> islub(D,X,x)";
   27.25 -by (safe_tac (claset()));
   27.26 +by Safe_tac;
   27.27  by (REPEAT(ares_tac prems 1));
   27.28  qed "islubI";
   27.29  
   27.30  val prems = goalw Limit.thy [isub_def]  (* isubI *)
   27.31      "[|x:set(D);  !!n. n:nat ==> rel(D,X`n,x)|] ==> isub(D,X,x)";
   27.32 -by (safe_tac (claset()));
   27.33 +by Safe_tac;
   27.34  by (REPEAT(ares_tac prems 1));
   27.35  qed "isubI";
   27.36  
   27.37  val prems = goalw Limit.thy [isub_def]  (* isubE *)
   27.38      "!!z.[|isub(D,X,x);[|x:set(D);  !!n. n:nat==>rel(D,X`n,x)|] ==> P|] ==> P";
   27.39 -by (safe_tac (claset()));
   27.40 +by Safe_tac;
   27.41  by (Asm_simp_tac 1);
   27.42  qed "isubE";
   27.43  
   27.44 @@ -236,7 +236,7 @@
   27.45  by (assume_tac 3);
   27.46  by (rtac (hd prems) 2);
   27.47  by (res_inst_tac [("n","m")] nat_induct 1);
   27.48 -by (safe_tac (claset()));
   27.49 +by Safe_tac;
   27.50  by (asm_full_simp_tac (simpset() addsimps prems) 2);
   27.51  by (rtac cpo_trans 4);
   27.52  by (rtac (le_succ_eq RS subst) 3);
   27.53 @@ -264,7 +264,7 @@
   27.54      "pcpo(D) ==> EX! x. x:set(D) & (ALL y:set(D). rel(D,x,y))";
   27.55  by (rtac (hd prems RS conjunct2 RS bexE) 1);
   27.56  by (rtac ex1I 1);
   27.57 -by (safe_tac (claset()));
   27.58 +by Safe_tac;
   27.59  by (assume_tac 1);
   27.60  by (etac bspec 1);
   27.61  by (assume_tac 1);
   27.62 @@ -338,7 +338,7 @@
   27.63  val prems = goalw Limit.thy [isub_def,suffix_def]  (* isub_suffix *)
   27.64      "[|chain(D,X); cpo(D); n:nat|] ==> isub(D,suffix(X,n),x) <-> isub(D,X,x)";
   27.65  by (simp_tac (simpset() addsimps prems) 1);
   27.66 -by (safe_tac (claset()));
   27.67 +by Safe_tac;
   27.68  by (dtac bspec 2);
   27.69  by (assume_tac 3);      (* to instantiate unknowns properly *)
   27.70  by (rtac cpo_trans 1);
   27.71 @@ -479,13 +479,13 @@
   27.72  
   27.73  val prems = goalw Limit.thy [matrix_def]  (* matrix_sym_axis *)
   27.74      "!!z. matrix(D,M) ==> matrix(D,lam m:nat. lam n:nat. M`n`m)";
   27.75 -by (Simp_tac 1 THEN safe_tac (claset()) THEN 
   27.76 +by (Simp_tac 1 THEN Safe_tac THEN 
   27.77  REPEAT(asm_simp_tac (simpset() addsimps [fun_swap]) 1));
   27.78  qed "matrix_sym_axis";
   27.79  
   27.80  val prems = goalw Limit.thy [chain_def]  (* matrix_chain_diag *)
   27.81      "matrix(D,M) ==> chain(D,lam n:nat. M`n`n)";
   27.82 -by (safe_tac (claset()));
   27.83 +by Safe_tac;
   27.84  by (rtac lam_type 1);
   27.85  by (rtac matrix_in 1);
   27.86  by (REPEAT(ares_tac prems 1));
   27.87 @@ -496,7 +496,7 @@
   27.88  
   27.89  val prems = goalw Limit.thy [chain_def]  (* matrix_chain_left *)
   27.90      "[|matrix(D,M); n:nat|] ==> chain(D,M`n)";
   27.91 -by (safe_tac (claset()));
   27.92 +by Safe_tac;
   27.93  by (rtac apply_type 1);
   27.94  by (rtac matrix_fun 1);
   27.95  by (REPEAT(ares_tac prems 1));
   27.96 @@ -506,7 +506,7 @@
   27.97  
   27.98  val prems = goalw Limit.thy [chain_def]  (* matrix_chain_right *)
   27.99      "[|matrix(D,M); m:nat|] ==> chain(D,lam n:nat. M`n`m)";
  27.100 -by (safe_tac (claset()));
  27.101 +by Safe_tac;
  27.102  by (asm_simp_tac(simpset() addsimps prems) 2);
  27.103  brr(lam_type::matrix_in::matrix_rel_1_0::prems) 1;
  27.104  qed "matrix_chain_right";
  27.105 @@ -537,7 +537,7 @@
  27.106      "[|isub(D,(lam n:nat. M`n`n),y); matrix(D,M); cpo(D)|] ==>  \
  27.107  \    isub(D,(lam n:nat. lub(D,lam m:nat. M`n`m)),y)";
  27.108  by (rewtac isub_def);
  27.109 -by (safe_tac (claset()));
  27.110 +by Safe_tac;
  27.111  by (rtac isubD1 1);
  27.112  by (resolve_tac prems 1);
  27.113  by (Asm_simp_tac 1);
  27.114 @@ -551,11 +551,11 @@
  27.115  by (assume_tac 1);
  27.116  by (resolve_tac prems 1);
  27.117  by (rewtac isub_def);
  27.118 -by (safe_tac (claset()));
  27.119 +by Safe_tac;
  27.120  by (rtac isubD1 1);
  27.121  by (resolve_tac prems 1);
  27.122  by (cut_inst_tac[("P","n le na")]excluded_middle 1);
  27.123 -by (safe_tac (claset()));
  27.124 +by Safe_tac;
  27.125  by (rtac cpo_trans 1);
  27.126  by (resolve_tac prems 1);
  27.127  by (rtac (not_le_iff_lt RS iffD1 RS leI RS chain_rel_gen) 1);
  27.128 @@ -575,7 +575,7 @@
  27.129  
  27.130  val prems = goalw Limit.thy [chain_def]  (* matrix_chain_lub *)
  27.131      "[|matrix(D,M); cpo(D)|] ==> chain(D,lam n:nat. lub(D,lam m:nat. M`n`m))";
  27.132 -by (safe_tac (claset()));
  27.133 +by Safe_tac;
  27.134  by (rtac lam_type 1);
  27.135  by (rtac islub_in 1);
  27.136  by (rtac cpo_lub 1);
  27.137 @@ -722,7 +722,7 @@
  27.138      "[|f:mono(D,E); chain(D,X)|] ==> chain(E,lam n:nat. f`(X`n))";
  27.139  by (rewtac chain_def);
  27.140  by (Simp_tac 1);
  27.141 -by (safe_tac (claset()));
  27.142 +by Safe_tac;
  27.143  by (rtac lam_type 1);
  27.144  by (rtac mono_map 1);
  27.145  by (resolve_tac prems 1);
  27.146 @@ -768,7 +768,7 @@
  27.147  \    rel(cf(D,E),f,g)";
  27.148  by (rtac rel_I 1);
  27.149  by (simp_tac (simpset() addsimps [cf_def]) 1);
  27.150 -by (safe_tac (claset()));
  27.151 +by Safe_tac;
  27.152  brr prems 1;
  27.153  qed "rel_cfI";
  27.154  
  27.155 @@ -1218,7 +1218,7 @@
  27.156  
  27.157  val prems = goalw Limit.thy [projpair_def]  (* projpair_id *)
  27.158      "cpo(D) ==> projpair(D,D,id(set(D)),id(set(D)))";
  27.159 -by (safe_tac (claset()));
  27.160 +by Safe_tac;
  27.161  brr(id_cont::id_comp::id_type::prems) 1;
  27.162  by (stac id_comp 1); (* Matches almost anything *)
  27.163  brr(id_cont::id_type::cpo_refl::cpo_cf::cont_cf::prems) 1;
  27.164 @@ -1245,7 +1245,7 @@
  27.165  val prems = goalw Limit.thy [projpair_def]  (* lemma *)
  27.166      "[|emb(D,D',e); emb(D',E,e'); cpo(D); cpo(D'); cpo(E)|] ==>  \
  27.167  \    projpair(D,E,e' O e,(Rp(D,D',e)) O (Rp(D',E,e')))";
  27.168 -by (safe_tac (claset()));
  27.169 +by Safe_tac;
  27.170  brr(comp_pres_cont::Rp_cont::emb_cont::prems) 1;
  27.171  by (rtac (comp_assoc RS subst) 1);
  27.172  by (res_inst_tac[("t1","e'")](comp_assoc RS ssubst) 1);
  27.173 @@ -1317,7 +1317,7 @@
  27.174  \      g:(PROD n:nat. set(DD`n))|] ==> rel(iprod(DD),f,g)";
  27.175  by (rtac rel_I 1);
  27.176  by (Simp_tac 1);
  27.177 -by (safe_tac (claset()));
  27.178 +by Safe_tac;
  27.179  brr prems 1;
  27.180  qed "rel_iprodI";
  27.181  
  27.182 @@ -1325,7 +1325,7 @@
  27.183      "[|rel(iprod(DD),f,g); n:nat|] ==> rel(DD`n,f`n,g`n)";
  27.184  by (cut_facts_tac[hd prems RS rel_E]1);
  27.185  by (Asm_full_simp_tac 1);
  27.186 -by (safe_tac (claset()));
  27.187 +by Safe_tac;
  27.188  by (etac bspec 1);
  27.189  by (resolve_tac prems 1);
  27.190  qed "rel_iprodE";
  27.191 @@ -1336,7 +1336,7 @@
  27.192  val prems = goalw Limit.thy [chain_def]  (* chain_iprod *)
  27.193      "[|chain(iprod(DD),X);  !!n. n:nat ==> cpo(DD`n); n:nat|] ==>  \
  27.194  \    chain(DD`n,lam m:nat. X`m`n)";
  27.195 -by (safe_tac (claset()));
  27.196 +by Safe_tac;
  27.197  by (rtac lam_type 1);
  27.198  by (rtac apply_type 1);
  27.199  by (rtac iprodE 1);
  27.200 @@ -1351,7 +1351,7 @@
  27.201  val prems = goalw Limit.thy [islub_def,isub_def]  (* islub_iprod *)
  27.202      "[|chain(iprod(DD),X);  !!n. n:nat ==> cpo(DD`n)|] ==>   \
  27.203  \    islub(iprod(DD),X,lam n:nat. lub(DD`n,lam m:nat. X`m`n))";
  27.204 -by (safe_tac (claset()));
  27.205 +by Safe_tac;
  27.206  by (rtac iprodI 1);
  27.207  by (rtac lam_type 1); 
  27.208  brr((chain_iprod RS cpo_lub RS islub_in)::prems) 1;
  27.209 @@ -1366,7 +1366,7 @@
  27.210  by (Asm_simp_tac 1);
  27.211  brr(islub_least::(chain_iprod RS cpo_lub)::prems) 1;
  27.212  by (rewtac isub_def);
  27.213 -by (safe_tac (claset()));
  27.214 +by Safe_tac;
  27.215  by (etac (iprodE RS apply_type) 1);
  27.216  by (assume_tac 1);
  27.217  by (Asm_simp_tac 1);
  27.218 @@ -1403,7 +1403,7 @@
  27.219      "[|set(D)<=set(E);  \
  27.220  \      !!x y. [|x:set(D); y:set(D)|] ==> rel(D,x,y)<->rel(E,x,y);  \
  27.221  \      !!X. chain(D,X) ==> lub(E,X) : set(D)|] ==> subcpo(D,E)";
  27.222 -by (safe_tac (claset()));
  27.223 +by Safe_tac;
  27.224  by (asm_full_simp_tac(simpset() addsimps prems) 2);
  27.225  by (asm_simp_tac(simpset() addsimps prems) 2);
  27.226  brr(prems@[subsetD]) 1;
  27.227 @@ -1564,7 +1564,7 @@
  27.228  val prems = goalw Limit.thy [emb_chain_def]  (* emb_chainI *)
  27.229      "[|!!n. n:nat ==> cpo(DD`n);   \
  27.230  \      !!n. n:nat ==> emb(DD`n,DD`succ(n),ee`n)|] ==> emb_chain(DD,ee)";
  27.231 -by (safe_tac (claset()));
  27.232 +by Safe_tac;
  27.233  brr prems 1;
  27.234  qed "emb_chainI";
  27.235  
  27.236 @@ -1702,7 +1702,7 @@
  27.237  by (res_inst_tac[("n","x")]nat_induct 1);
  27.238  by (resolve_tac prems 1);
  27.239  by (Fast_tac 1);
  27.240 -by (safe_tac (claset()));
  27.241 +by Safe_tac;
  27.242  by (Asm_simp_tac 1);
  27.243  by (Asm_simp_tac 1);
  27.244  qed "succ_sub1";
  27.245 @@ -1713,7 +1713,7 @@
  27.246  by (resolve_tac prems 1);
  27.247  by (rtac impI 1);
  27.248  by (asm_full_simp_tac(simpset() addsimps prems) 1);
  27.249 -by (safe_tac (claset()));
  27.250 +by Safe_tac;
  27.251  by (asm_full_simp_tac(simpset() addsimps prems) 1); (* Surprise, surprise. *)
  27.252  qed "succ_le_pos";
  27.253  
  27.254 @@ -1721,7 +1721,7 @@
  27.255      "!!z. [|n:nat; m:nat|] ==> m le n --> (EX k:nat. n = m #+ k)";
  27.256  by (res_inst_tac[("n","m")]nat_induct 1);
  27.257  by (assume_tac 1);
  27.258 -by (safe_tac (claset()));
  27.259 +by Safe_tac;
  27.260  by (rtac bexI 1);
  27.261  by (rtac (add_0 RS sym) 1);
  27.262  by (assume_tac 1);
  27.263 @@ -1828,7 +1828,7 @@
  27.264  brr(add_le_mono::nat_le_refl::add_type::nat_succI::prems) 1;
  27.265  by (stac comp_assoc 1);
  27.266  brr(comp_mono_eq::refl::[]) 1;
  27.267 -(* by(asm_simp_tac ZF_ss 1); *)
  27.268 +(* by (asm_simp_tac ZF_ss 1); *)
  27.269  by (asm_simp_tac(ZF_ss addsimps(e_less_eq::add_type::nat_succI::prems)) 1);
  27.270  by (stac id_comp 1); (* simp cannot unify/inst right, use brr below(?). *)
  27.271  brr((emb_e_less_add RS emb_cont RS cont_fun)::refl::nat_succI::prems) 1;
  27.272 @@ -2012,7 +2012,7 @@
  27.273  by (stac id_comp 1);
  27.274  brr((e_less_cont RS cont_fun)::add_type::add_le_mono::nat_le_refl::refl::
  27.275      prems) 1;
  27.276 -by(asm_full_simp_tac(ZF_ss addsimps(e_less_eq::nat_succI::add_type::prems)) 1);
  27.277 +by (asm_full_simp_tac(ZF_ss addsimps(e_less_eq::nat_succI::add_type::prems)) 1);
  27.278  by (stac comp_id 1);
  27.279  brr((e_gr_cont RS cont_fun)::add_type::nat_succI::add_le_self::refl::prems) 1;
  27.280  qed "e_gr_e_less_split_add";
  27.281 @@ -2029,7 +2029,7 @@
  27.282      "[|emb_chain(DD,ee); m:nat; n:nat|] ==>   \
  27.283  \    eps(DD,ee,m,n): set(DD`m)->set(DD`n)";
  27.284  by (rtac (expand_if RS iffD2) 1);
  27.285 -by (safe_tac (claset()));
  27.286 +by Safe_tac;
  27.287  brr((e_less_cont RS cont_fun)::prems) 1;
  27.288  brr((not_le_iff_lt RS iffD1 RS leI)::e_gr_fun::nat_into_Ord::prems) 1;
  27.289  qed "eps_fun";
  27.290 @@ -2051,7 +2051,7 @@
  27.291  val prems = goalw Limit.thy [eps_def]  (* eps_e_gr_add *)
  27.292      "[|n:nat; k:nat|] ==> eps(DD,ee,n#+k,n) = e_gr(DD,ee,n#+k,n)";
  27.293  by (rtac (expand_if RS iffD2) 1);
  27.294 -by (safe_tac (claset()));
  27.295 +by Safe_tac;
  27.296  by (etac leE 1);
  27.297  (* Must control rewriting by instantiating a variable. *)
  27.298  by (asm_full_simp_tac(simpset() addsimps
  27.299 @@ -2433,7 +2433,7 @@
  27.300    "[| !!n. n:nat ==> emb(DD`n,E,r(n));   \
  27.301  \     !!m n. [|m le n; m:nat; n:nat|] ==> r(n) O eps(DD,ee,m,n) = r(m) |] ==>  \
  27.302  \  commute(DD,ee,E,r)";
  27.303 -by (safe_tac (claset()));
  27.304 +by Safe_tac;
  27.305  brr prems 1;
  27.306  qed "commuteI";
  27.307  
  27.308 @@ -2663,7 +2663,7 @@
  27.309  \   (E,G,   \
  27.310  \    lub(cf(E,G), lam n:nat. f(n) O Rp(DD`n,E,r(n))),  \
  27.311  \    lub(cf(G,E), lam n:nat. r(n) O Rp(DD`n,G,f(n))))";
  27.312 -by (safe_tac (claset()));
  27.313 +by Safe_tac;
  27.314  by (stac comp_lubs 3);
  27.315  (* The following one line is 15 lines in HOL, and includes existentials. *)
  27.316  brr(cf_cont::islub_in::cpo_lub::cpo_cf::theta_chain::theta_proj_chain::prems) 1;
  27.317 @@ -2759,7 +2759,7 @@
  27.318  
  27.319  val mediatingI = prove_goalw Limit.thy [mediating_def]
  27.320    "[|emb(E,G,t);  !!n. n:nat ==> f(n) = t O r(n) |]==>mediating(E,G,r,f,t)"
  27.321 - (fn prems => [safe_tac (claset()),trr prems 1]);
  27.322 + (fn prems => [Safe_tac,trr prems 1]);
  27.323  
  27.324  val mediating_emb = prove_goalw Limit.thy [mediating_def]
  27.325    "!!z. mediating(E,G,r,f,t) ==> emb(E,G,t)"
  27.326 @@ -2816,7 +2816,7 @@
  27.327  \  (ALL t. mediating(Dinf(DD,ee),G,rho_emb(DD,ee),f,t) -->  \
  27.328  \    t = lub(cf(Dinf(DD,ee),G),   \
  27.329  \        lam n:nat. f(n) O Rp(DD`n,Dinf(DD,ee),rho_emb(DD,ee,n))))";
  27.330 -by (safe_tac (claset()));
  27.331 +by Safe_tac;
  27.332  brr(lub_universal_mediating::rho_emb_commute::rho_emb_lub::cpo_Dinf::prems) 1;
  27.333  brr(lub_universal_unique::rho_emb_commute::rho_emb_lub::cpo_Dinf::prems) 1;
  27.334  qed "Dinf_universal";
    28.1 --- a/src/ZF/ex/Mutil.ML	Wed Nov 05 11:49:34 1997 +0100
    28.2 +++ b/src/ZF/ex/Mutil.ML	Wed Nov 05 13:14:15 1997 +0100
    28.3 @@ -76,7 +76,7 @@
    28.4  
    28.5  goal thy "!!t. t:tiling(domino) ==> Finite(t)";
    28.6  by (eresolve_tac [tiling.induct] 1);
    28.7 -by (resolve_tac [Finite_0] 1);
    28.8 +by (rtac Finite_0 1);
    28.9  by (blast_tac (claset() addSIs [Finite_Un] addIs [domino_Finite]) 1);
   28.10  qed "tiling_domino_Finite";
   28.11  
   28.12 @@ -121,8 +121,8 @@
   28.13  \                   t = (succ(m)#+succ(m))*(succ(n)#+succ(n));  \
   28.14  \                   t' = t - {<0,0>} - {<succ(m#+m), succ(n#+n)>} |] ==> \
   28.15  \                t' ~: tiling(domino)";
   28.16 -by (resolve_tac [notI] 1);
   28.17 -by (dresolve_tac [tiling_domino_0_1] 1);
   28.18 +by (rtac notI 1);
   28.19 +by (dtac tiling_domino_0_1 1);
   28.20  by (subgoal_tac "|evnodd(t',0)| < |evnodd(t',1)|" 1);
   28.21  by (asm_full_simp_tac (simpset() addsimps [lt_not_refl]) 1);
   28.22  by (subgoal_tac "t : tiling(domino)" 1);
   28.23 @@ -134,7 +134,7 @@
   28.24  by (asm_full_simp_tac 
   28.25      (simpset() addsimps [evnodd_Diff, mod2_add_self,
   28.26                          mod2_succ_succ, tiling_domino_0_1 RS sym]) 1);
   28.27 -by (resolve_tac [lt_trans] 1);
   28.28 +by (rtac lt_trans 1);
   28.29  by (REPEAT
   28.30      (rtac Finite_imp_cardinal_Diff 1 
   28.31       THEN
    29.1 --- a/src/ZF/ex/Ntree.ML	Wed Nov 05 11:49:34 1997 +0100
    29.2 +++ b/src/ZF/ex/Ntree.ML	Wed Nov 05 13:14:15 1997 +0100
    29.3 @@ -58,7 +58,7 @@
    29.4  goalw Ntree.thy (ntree.defs@ntree.con_defs) "ntree(univ(A)) <= univ(A)";
    29.5  by (rtac lfp_lowerbound 1);
    29.6  by (rtac (A_subset_univ RS univ_mono) 2);
    29.7 -by (safe_tac (claset()));
    29.8 +by Safe_tac;
    29.9  by (REPEAT (ares_tac [Pair_in_univ, nat_fun_univ RS subsetD] 1));
   29.10  qed "ntree_univ";
   29.11  
    30.1 --- a/src/ZF/ex/Primes.ML	Wed Nov 05 11:49:34 1997 +0100
    30.2 +++ b/src/ZF/ex/Primes.ML	Wed Nov 05 13:14:15 1997 +0100
    30.3 @@ -150,7 +150,7 @@
    30.4  by (asm_simp_tac (simpset() addsimps [egcd_0,dvd_refl,dvd_0_right,
    30.5                                       dvd_imp_nat2]) 2);
    30.6  (* case x > 0 *)
    30.7 -by (safe_tac (claset()));
    30.8 +by Safe_tac;
    30.9  by (asm_simp_tac (simpset() addsimps [egcd_lt_0, nat_into_Ord RS Ord_0_lt,
   30.10                                       dvd_imp_nat2]) 1);
   30.11  by (eres_inst_tac [("x","a mod x")] ballE 1);
    31.1 --- a/src/ZF/ex/Primrec.ML	Wed Nov 05 11:49:34 1997 +0100
    31.2 +++ b/src/ZF/ex/Primrec.ML	Wed Nov 05 13:14:15 1997 +0100
    31.3 @@ -273,7 +273,7 @@
    31.4  by (DO_GOAL [res_inst_tac [("x","0")] bexI,
    31.5               asm_simp_tac (simpset() addsimps [lt_ack1, nat_0_le]),
    31.6               resolve_tac nat_typechecks] 1);
    31.7 -by (safe_tac (claset()));
    31.8 +by Safe_tac;
    31.9  by (Asm_simp_tac 1);
   31.10  by (rtac (ballI RS bexI) 1);
   31.11  by (rtac (add_lt_mono RS lt_trans) 1);
   31.12 @@ -352,7 +352,7 @@
   31.13  goal Primrec.thy
   31.14      "!!f. f:primrec ==> EX k:nat. ALL l:list(nat). f`l < ack(k, list_add(l))";
   31.15  by (etac primrec.induct 1);
   31.16 -by (safe_tac (claset()));
   31.17 +by Safe_tac;
   31.18  by (DEPTH_SOLVE
   31.19      (ares_tac ([SC_case, CONST_case, PROJ_case, COMP_case, PREC_case,
   31.20                         bexI, ballI] @ nat_typechecks) 1));
    32.1 --- a/src/ZF/ex/PropLog.ML	Wed Nov 05 11:49:34 1997 +0100
    32.2 +++ b/src/ZF/ex/PropLog.ML	Wed Nov 05 13:14:15 1997 +0100
    32.3 @@ -263,7 +263,7 @@
    32.4      "[| p: prop;  0 |= p |] ==> ALL t. hyps(p,t) - hyps(p,t0) |- p";
    32.5  by (rtac (premp RS hyps_finite RS Fin_induct) 1);
    32.6  by (simp_tac (simpset() addsimps [premp, sat, logcon_thms_p, Diff_0]) 1);
    32.7 -by (safe_tac (claset()));
    32.8 +by Safe_tac;
    32.9  (*Case hyps(p,t)-cons(#v,Y) |- p *)
   32.10  by (rtac thms_excluded_middle_rule 1);
   32.11  by (etac prop.Var_I 3);
    33.1 --- a/src/ZF/ex/Ramsey.ML	Wed Nov 05 11:49:34 1997 +0100
    33.2 +++ b/src/ZF/ex/Ramsey.ML	Wed Nov 05 13:14:15 1997 +0100
    33.3 @@ -88,7 +88,7 @@
    33.4  by (nat_ind_tac "n" [] 1);
    33.5  by (fast_tac (claset() addSIs [Atleast0]) 1);
    33.6  by (asm_simp_tac (simpset() addsimps [add_succ_right]) 1);
    33.7 -by (safe_tac (claset()));
    33.8 +by Safe_tac;
    33.9  by (etac (Atleast_succD RS bexE) 1);
   33.10  by (etac UnE 1);
   33.11  (**case x:B.  Instantiate the 'ALL A B' induction hypothesis. **)
   33.12 @@ -165,7 +165,7 @@
   33.13     "[| Ramsey(succ(m), succ(i), j);  Ramsey(n, i, succ(j));  \
   33.14  \      m: nat;  n: nat |] ==> \
   33.15  \   Ramsey(succ(m#+n), succ(i), succ(j))";
   33.16 -by (safe_tac (claset()));
   33.17 +by Safe_tac;
   33.18  by (etac (Atleast_succD RS bexE) 1);
   33.19  by (eres_inst_tac [("P1","%z.<x,z>:E")] (Atleast_partition RS disjE) 1);
   33.20  by (REPEAT (resolve_tac prems 1));
   33.21 @@ -173,13 +173,13 @@
   33.22  by (rtac (ram1 RS spec RS spec RS mp RS disjE) 1);
   33.23  by (Fast_tac 1);
   33.24  by (fast_tac (claset() addEs [Clique_superset]) 1); (*easy -- given a Clique*)
   33.25 -by (safe_tac (claset()));
   33.26 +by Safe_tac;
   33.27  by (eresolve_tac (swapify [exI]) 1);             (*ignore main EX quantifier*)
   33.28  by (REPEAT (ares_tac [Indept_succ] 1));          (*make a bigger Indept*)
   33.29  (*case n*)
   33.30  by (rtac (ram2 RS spec RS spec RS mp RS disjE) 1);
   33.31  by (Fast_tac 1);
   33.32 -by (safe_tac (claset()));
   33.33 +by Safe_tac;
   33.34  by (rtac exI 1);
   33.35  by (REPEAT (ares_tac [Clique_succ] 1));          (*make a bigger Clique*)
   33.36  by (fast_tac (claset() addEs [Indept_superset]) 1); (*easy -- given an Indept*)
    34.1 --- a/src/ZF/ex/Term.ML	Wed Nov 05 11:49:34 1997 +0100
    34.2 +++ b/src/ZF/ex/Term.ML	Wed Nov 05 13:14:15 1997 +0100
    34.3 @@ -51,7 +51,7 @@
    34.4  goalw Term.thy (term.defs@term.con_defs) "term(univ(A)) <= univ(A)";
    34.5  by (rtac lfp_lowerbound 1);
    34.6  by (rtac (A_subset_univ RS univ_mono) 2);
    34.7 -by (safe_tac (claset()));
    34.8 +by Safe_tac;
    34.9  by (REPEAT (ares_tac [Pair_in_univ, list_univ RS subsetD] 1));
   34.10  qed "term_univ";
   34.11  
    35.1 --- a/src/ZF/ex/misc.ML	Wed Nov 05 11:49:34 1997 +0100
    35.2 +++ b/src/ZF/ex/misc.ML	Wed Nov 05 13:14:15 1997 +0100
    35.3 @@ -45,7 +45,7 @@
    35.4  \                    (ALL x:A. ALL y:A. H`(f`<x,y>) = g`<H`x,H`y>)}) --> \
    35.5  \    J : hom(A,f,B,g) & K : hom(B,g,C,h) -->  \
    35.6  \    (K O J) : hom(A,f,C,h)";
    35.7 -by (asm_simp_tac (simpset() setloop (K (safe_tac (claset())))) 1);
    35.8 +by (asm_simp_tac (simpset() setloop (K Safe_tac)) 1);
    35.9  val comp_homs = result();
   35.10  
   35.11  (*This version uses meta-level rewriting, safe_tac and asm_simp_tac*)
   35.12 @@ -56,7 +56,7 @@
   35.13  \    J : hom(A,f,B,g) & K : hom(B,g,C,h) -->  \
   35.14  \    (K O J) : hom(A,f,C,h)";
   35.15  by (rewtac hom_def);
   35.16 -by (safe_tac (claset()));
   35.17 +by Safe_tac;
   35.18  by (Asm_simp_tac 1);
   35.19  by (Asm_simp_tac 1);
   35.20  qed "comp_homs";