--- a/src/ZF/AC/AC10_AC15.ML Wed Nov 05 11:49:34 1997 +0100
+++ b/src/ZF/AC/AC10_AC15.ML Wed Nov 05 13:14:15 1997 +0100
@@ -141,7 +141,7 @@
(* ********************************************************************** *)
goalw thy AC_defs "!!Z. AC12 ==> AC15";
-by (safe_tac (claset()));
+by Safe_tac;
by (etac allE 1);
by (etac impE 1);
by (etac cons_times_nat_not_Finite 1);
@@ -167,7 +167,7 @@
(* ********************************************************************** *)
goalw thy AC_defs "!!n. [| n:nat; 1 le n; AC10(n) |] ==> AC13(n)";
-by (safe_tac (claset()));
+by Safe_tac;
by (fast_tac (empty_cs addSEs [allE, cons_times_nat_not_Finite RSN (2, impE),
ex_fun_AC13_AC15]) 1);
qed "AC10_AC13";
--- a/src/ZF/AC/WO2_AC16.ML Wed Nov 05 11:49:34 1997 +0100
+++ b/src/ZF/AC/WO2_AC16.ML Wed Nov 05 13:14:15 1997 +0100
@@ -48,7 +48,7 @@
\ ==> ALL y<x. ALL z<a. z < y | (EX Y:F(y). fa(z) <= Y) --> \
\ (EX! Y. Y : F(y) & fa(z) <= Y)";
by (REPEAT (resolve_tac [oallI, impI] 1));
-by (dresolve_tac [ospec] 1 THEN (assume_tac 1));
+by (dtac ospec 1 THEN (assume_tac 1));
by (fast_tac (FOL_cs addSEs [oallE]) 1);
val lemma4 = result();
@@ -62,7 +62,7 @@
by (rtac conjI 1);
by (rtac subsetI 1);
by (etac OUN_E 1);
-by (dresolve_tac [ospec] 1 THEN (assume_tac 1));
+by (dtac ospec 1 THEN (assume_tac 1));
by (Fast_tac 1);
by (dtac lemma4 1 THEN (assume_tac 1));
by (rtac oallI 1);
@@ -322,7 +322,7 @@
goal thy "!!j. [| ALL y<succ(j). F(y)<=X & (ALL x<a. x<y | P(x,y) \
\ --> Q(x,y)); succ(j)<a |] \
\ ==> F(j)<=X & (ALL x<a. x<j | P(x,j) --> Q(x,j))";
-by (dresolve_tac [ospec] 1);
+by (dtac ospec 1);
by (resolve_tac [lt_Ord RS (succI1 RS ltI RS lt_Ord RS le_refl)] 1
THEN (REPEAT (assume_tac 1)));
val lemma6 = result();
--- a/src/ZF/AC/WO6_WO1.ML Wed Nov 05 11:49:34 1997 +0100
+++ b/src/ZF/AC/WO6_WO1.ML Wed Nov 05 13:14:15 1997 +0100
@@ -21,7 +21,7 @@
qed "lt_oadd_odiff_disj";
(*The corresponding elimination rule*)
-val lt_oadd_odiff_cases = rule_by_tactic (safe_tac (claset()))
+val lt_oadd_odiff_cases = rule_by_tactic Safe_tac
(lt_oadd_odiff_disj RS disjE);
(* ********************************************************************** *)
@@ -353,7 +353,7 @@
goal thy "EX y. x Un y*y <= y";
by (res_inst_tac [("x","UN n:nat. rec(n, x, %k r. r Un r*r)")] exI 1);
-by (safe_tac (claset()));
+by Safe_tac;
by (rtac (nat_0I RS UN_I) 1);
by (Asm_simp_tac 1);
by (res_inst_tac [("a","succ(n Un na)")] UN_I 1);
--- a/src/ZF/AC/rel_is_fun.ML Wed Nov 05 11:49:34 1997 +0100
+++ b/src/ZF/AC/rel_is_fun.ML Wed Nov 05 13:14:15 1997 +0100
@@ -27,7 +27,7 @@
goalw Cardinal.thy [function_def]
"!!r. [| succ(m) lepoll domain(r); r lepoll succ(m); m:nat |] ==> \
\ function(r)";
-by (safe_tac (claset()));
+by Safe_tac;
by (resolve_tac [excluded_middle RS disjE] 1 THEN (atac 2));
by (fast_tac (claset() addSEs [lepoll_trans RS succ_lepoll_natE,
Diff_sing_lepoll RSN (2, lepoll_m_imp_domain_lepoll_m)]
--- a/src/ZF/Cardinal.ML Wed Nov 05 11:49:34 1997 +0100
+++ b/src/ZF/Cardinal.ML Wed Nov 05 13:14:15 1997 +0100
@@ -239,7 +239,7 @@
goal Cardinal.thy "Ord(LEAST x. P(x))";
by (excluded_middle_tac "EX i. Ord(i) & P(i)" 1);
-by (safe_tac (claset()));
+by Safe_tac;
by (rtac (Least_le RS ltE) 2);
by (REPEAT_SOME assume_tac);
by (etac (Least_0 RS ssubst) 1);
@@ -351,7 +351,7 @@
by (excluded_middle_tac "EX i. Ord(i) & i eqpoll A" 1);
by (etac (Least_0 RS ssubst) 1 THEN rtac Card_0 1);
by (rtac (Ord_Least RS CardI) 1);
-by (safe_tac (claset()));
+by Safe_tac;
by (rtac less_LeastE 1);
by (assume_tac 2);
by (etac eqpoll_trans 1);
@@ -433,7 +433,7 @@
goalw Cardinal.thy [lepoll_def, inj_def]
"!!A B. [| cons(u,A) lepoll cons(v,B); u~:A; v~:B |] ==> A lepoll B";
-by (safe_tac (claset()));
+by Safe_tac;
by (res_inst_tac [("x", "lam x:A. if(f`x=v, f`u, f`x)")] exI 1);
by (rtac CollectI 1);
(*Proving it's in the function space A->B*)
@@ -568,7 +568,7 @@
(*Congruence law for cons under equipollence*)
goalw Cardinal.thy [lepoll_def]
"!!A B. [| A lepoll B; b ~: B |] ==> cons(a,A) lepoll cons(b,B)";
-by (safe_tac (claset()));
+by Safe_tac;
by (res_inst_tac [("x", "lam y: cons(a,A).if(y=a, b, f`y)")] exI 1);
by (res_inst_tac [("d","%z. if(z:B, converse(f)`z, a)")]
lam_injective 1);
@@ -650,7 +650,7 @@
by (rtac cons_lepoll_consD 1);
by (rtac mem_not_refl 3);
by (eresolve_tac [cons_Diff RS ssubst] 1);
-by (safe_tac (claset()));
+by Safe_tac;
qed "Diff_sing_lepoll";
(*If A has at least n+1 elements then A-{a} has at least n.*)
--- a/src/ZF/CardinalArith.ML Wed Nov 05 11:49:34 1997 +0100
+++ b/src/ZF/CardinalArith.ML Wed Nov 05 13:14:15 1997 +0100
@@ -140,7 +140,7 @@
by (rtac exI 1);
by (res_inst_tac [("c", "%<x,y>.<y,x>"), ("d", "%<x,y>.<y,x>")]
lam_bijective 1);
-by (safe_tac (claset()));
+by Safe_tac;
by (ALLGOALS (Asm_simp_tac));
qed "prod_commute_eqpoll";
@@ -192,7 +192,7 @@
goalw CardinalArith.thy [eqpoll_def] "0*A eqpoll 0";
by (rtac exI 1);
by (rtac lam_bijective 1);
-by (safe_tac (claset()));
+by Safe_tac;
qed "prod_0_eqpoll";
goalw CardinalArith.thy [cmult_def] "0 |*| i = 0";
@@ -604,7 +604,7 @@
by (rewtac Transset_def);
by (safe_tac subset_cs);
by (asm_full_simp_tac (simpset() addsimps [ordertype_pred_unfold]) 1);
-by (safe_tac (claset()));
+by Safe_tac;
by (rtac UN_I 1);
by (rtac ReplaceI 2);
by (ALLGOALS (blast_tac (claset() addIs [well_ord_subset] addSEs [predE])));
--- a/src/ZF/Coind/ECR.ML Wed Nov 05 11:49:34 1997 +0100
+++ b/src/ZF/Coind/ECR.ML Wed Nov 05 13:14:15 1997 +0100
@@ -49,7 +49,7 @@
goalw ECR.thy [hastyenv_def]
"!!ve.[| ve:ValEnv; te:TyEnv; hastyenv(ve,te); <v,t>:HasTyRel |] ==> \
\ hastyenv(ve_owr(ve,x,v),te_owr(te,x,t))";
-by (safe_tac (claset()));
+by Safe_tac;
by (stac ve_dom_owr 1);
by (assume_tac 1);
by (etac (HasTyRel.dom_subset RS subsetD RS SigmaD1 RS ValNEE) 1);
@@ -69,10 +69,10 @@
goalw ECR.thy [isofenv_def,hastyenv_def]
"!!ve.[| ve:ValEnv; te:TyEnv; isofenv(ve,te) |] ==> hastyenv(ve,te)";
-by (safe_tac (claset()));
+by Safe_tac;
by (dtac bspec 1);
by (assume_tac 1);
-by (safe_tac (claset()));
+by Safe_tac;
by (dtac HasTyRel.htr_constI 1);
by (assume_tac 2);
by (etac te_appI 1);
--- a/src/ZF/Coind/MT.ML Wed Nov 05 11:49:34 1997 +0100
+++ b/src/ZF/Coind/MT.ML Wed Nov 05 13:14:15 1997 +0100
@@ -51,7 +51,7 @@
\ <cl,t>:HasTyRel";
by (cut_facts_tac prems 1);
by (etac elab_fixE 1);
-by (safe_tac (claset()));
+by Safe_tac;
by (EVERY [forward_tac [subst] 1,atac 2,rtac htr_closCI 1]);
by clean_tac;
by (rtac ve_owrI 1);
@@ -129,7 +129,7 @@
by (etac htr_closE 1);
by (etac elab_fnE 1);
by (rewrite_tac Ty.con_defs);
-by (safe_tac (claset()));
+by Safe_tac;
by (dtac (spec RS spec RS mp RS mp) 1);
by (assume_tac 3);
by (assume_tac 2);
--- a/src/ZF/Coind/Map.ML Wed Nov 05 11:49:34 1997 +0100
+++ b/src/ZF/Coind/Map.ML Wed Nov 05 13:14:15 1997 +0100
@@ -69,7 +69,7 @@
(** map_emp **)
goalw Map.thy [map_emp_def,PMap_def,TMap_def] "map_emp:PMap(A,B)";
-by (safe_tac (claset()));
+by Safe_tac;
by (rtac image_02 1);
qed "pmap_empI";
@@ -89,7 +89,7 @@
by (dres_inst_tac [("psi", "?uu ~: B")] asm_rl 1);
by (asm_full_simp_tac
(simpset() addsimps [qbeta] setloop split_tac [expand_if]) 1);
-by (safe_tac (claset()));
+by Safe_tac;
by (dres_inst_tac [("psi", "?uu ~: B")] asm_rl 3);
by (ALLGOALS Asm_full_simp_tac);
by (Fast_tac 1);
--- a/src/ZF/EquivClass.ML Wed Nov 05 11:49:34 1997 +0100
+++ b/src/ZF/EquivClass.ML Wed Nov 05 13:14:15 1997 +0100
@@ -143,7 +143,7 @@
\ !!x. x : A ==> b(x) : B |] \
\ ==> (UN x:X. b(x)) : B";
by (cut_facts_tac prems 1);
-by (safe_tac (claset()));
+by Safe_tac;
by (asm_simp_tac (simpset() addsimps (UN_equiv_class::prems)) 1);
qed "UN_equiv_class_type";
@@ -156,7 +156,7 @@
\ !!x y. [| x:A; y:A; b(x)=b(y) |] ==> <x,y>:r |] \
\ ==> X=Y";
by (cut_facts_tac prems 1);
-by (safe_tac (claset()));
+by Safe_tac;
by (rtac equiv_class_eq 1);
by (REPEAT (ares_tac prems 1));
by (etac box_equals 1);
@@ -176,7 +176,7 @@
"[| equiv(A,r); congruent2(r,b); a: A |] ==> \
\ congruent(r, %x1. UN x2:r``{a}. b(x1,x2))";
by (cut_facts_tac (equivA::prems) 1);
-by (safe_tac (claset()));
+by Safe_tac;
by (rtac (equivA RS equiv_type RS subsetD RS SigmaE2) 1);
by (assume_tac 1);
by (asm_simp_tac (simpset() addsimps [equivA RS UN_equiv_class,
@@ -201,7 +201,7 @@
\ !!x1 x2. [| x1: A; x2: A |] ==> b(x1,x2) : B \
\ |] ==> (UN x1:X1. UN x2:X2. b(x1,x2)) : B";
by (cut_facts_tac prems 1);
-by (safe_tac (claset()));
+by Safe_tac;
by (REPEAT (ares_tac (prems@[UN_equiv_class_type,
congruent2_implies_congruent_UN,
congruent2_implies_congruent, quotientI]) 1));
@@ -216,7 +216,7 @@
\ !! y z w. [| w: A; <y,z> : r |] ==> b(w,y) = b(w,z) \
\ |] ==> congruent2(r,b)";
by (cut_facts_tac prems 1);
-by (safe_tac (claset()));
+by Safe_tac;
by (rtac trans 1);
by (REPEAT (ares_tac prems 1
ORELSE etac (subsetD RS SigmaE2) 1 THEN assume_tac 2 THEN assume_tac 1));
@@ -244,7 +244,7 @@
val congt' = rewrite_rule [congruent_def] congt;
by (cut_facts_tac [ZinA] 1);
by (rewtac congruent_def);
-by (safe_tac (claset()));
+by Safe_tac;
by (rtac (equivA RS equiv_type RS subsetD RS SigmaE2) 1);
by (assume_tac 1);
by (asm_simp_tac (simpset() addsimps [commute,
--- a/src/ZF/Finite.ML Wed Nov 05 11:49:34 1997 +0100
+++ b/src/ZF/Finite.ML Wed Nov 05 13:14:15 1997 +0100
@@ -60,7 +60,7 @@
by (etac Fin_induct 1);
by (simp_tac (simpset() addsimps [subset_empty_iff]) 1);
by (asm_simp_tac (simpset() addsimps subset_cons_iff::distrib_simps) 1);
-by (safe_tac (claset()));
+by Safe_tac;
by (eres_inst_tac [("b","z")] (cons_Diff RS subst) 1);
by (Asm_simp_tac 1);
qed "Fin_subset_lemma";
@@ -131,7 +131,7 @@
by (etac FiniteFun.induct 1);
by (simp_tac (simpset() addsimps subset_empty_iff::FiniteFun.intrs) 1);
by (asm_simp_tac (simpset() addsimps subset_cons_iff::distrib_simps) 1);
-by (safe_tac (claset()));
+by Safe_tac;
by (eres_inst_tac [("b","z")] (cons_Diff RS subst) 1);
by (dtac (spec RS mp) 1 THEN assume_tac 1);
by (fast_tac (claset() addSIs FiniteFun.intrs) 1);
--- a/src/ZF/IMP/Equiv.ML Wed Nov 05 11:49:34 1997 +0100
+++ b/src/ZF/IMP/Equiv.ML Wed Nov 05 13:14:15 1997 +0100
@@ -90,7 +90,7 @@
"c : com ==> ALL x:C(c). <c,fst(x)> -c-> snd(x)";
by (rtac (prem RS com.induct) 1);
by (rewrite_tac C_rewrite_rules);
-by (safe_tac (claset()));
+by Safe_tac;
by (ALLGOALS Asm_full_simp_tac);
(* skip *)
@@ -107,7 +107,7 @@
(* while *)
by (EVERY1 [forward_tac [Gamma_bnd_mono], etac induct, atac]);
by (rewtac Gamma_def);
-by (safe_tac (claset()));
+by Safe_tac;
by (EVERY1 [dtac bspec, atac]);
by (ALLGOALS Asm_full_simp_tac);
--- a/src/ZF/Order.ML Wed Nov 05 11:49:34 1997 +0100
+++ b/src/ZF/Order.ML Wed Nov 05 13:14:15 1997 +0100
@@ -44,12 +44,12 @@
goalw Order.thy [well_ord_def]
"!!r. well_ord(A,r) ==> wf[A](r)";
-by (safe_tac (claset()));
+by Safe_tac;
qed "well_ord_is_wf";
goalw Order.thy [well_ord_def, tot_ord_def, part_ord_def]
"!!r. well_ord(A,r) ==> trans[A](r)";
-by (safe_tac (claset()));
+by Safe_tac;
qed "well_ord_is_trans_on";
goalw Order.thy [well_ord_def, tot_ord_def]
@@ -274,7 +274,7 @@
goalw Order.thy [ord_iso_def, mono_map_def]
"!!f g. [| f: mono_map(A,r,B,s); g: mono_map(B,s,A,r); \
\ f O g = id(B); g O f = id(A) |] ==> f: ord_iso(A,r,B,s)";
-by (safe_tac (claset()));
+by Safe_tac;
by (REPEAT_FIRST (ares_tac [fg_imp_bijective]));
by (Blast_tac 1);
by (subgoal_tac "<g`(f`x), g`(f`y)> : r" 1);
@@ -305,7 +305,7 @@
goalw Order.thy [linear_def, ord_iso_def]
"!!A B r. [| linear(B,s); f: ord_iso(A,r,B,s) |] ==> linear(A,r)";
by (Asm_simp_tac 1);
-by (safe_tac (claset()));
+by Safe_tac;
by (dres_inst_tac [("x1", "f`x"), ("x", "f`xa")] (bspec RS bspec) 1);
by (safe_tac (claset() addSEs [bij_is_fun RS apply_type]));
by (dres_inst_tac [("t", "op `(converse(f))")] subst_context 1);
@@ -316,7 +316,7 @@
"!!A B r. [| wf[B](s); f: ord_iso(A,r,B,s) |] ==> wf[A](r)";
(*reversed &-congruence rule handles context of membership in A*)
by (asm_full_simp_tac (simpset() addcongs [conj_cong2]) 1);
-by (safe_tac (claset()));
+by Safe_tac;
by (dres_inst_tac [("x", "{f`z. z:Z Int A}")] spec 1);
by (safe_tac (claset() addSIs [equalityI]));
by (ALLGOALS (blast_tac
@@ -430,7 +430,7 @@
by (forward_tac [well_ord_iso_subset_lemma] 1);
by (res_inst_tac [("f","converse(f)"), ("g","g")] ord_iso_trans 1);
by (REPEAT_FIRST (ares_tac [subset_refl, ord_iso_sym]));
-by (safe_tac (claset()));
+by Safe_tac;
by (forward_tac [ord_iso_converse] 1);
by (EVERY (map (blast_tac bij_apply_cs) [1,1,1]));
by (asm_full_simp_tac bij_inverse_ss 1);
@@ -489,7 +489,7 @@
\ : mono_map(domain(ord_iso_map(A,r,B,s)), r, \
\ range(ord_iso_map(A,r,B,s)), s)";
by (asm_simp_tac (simpset() addsimps [ord_iso_map_fun]) 1);
-by (safe_tac (claset()));
+by Safe_tac;
by (subgoals_tac ["x:A", "xa:A", "y:B", "ya:B"] 1);
by (REPEAT
(blast_tac (claset() addSEs [ord_iso_map_subset RS subsetD RS SigmaE]) 2));
--- a/src/ZF/OrderArith.ML Wed Nov 05 11:49:34 1997 +0100
+++ b/src/ZF/OrderArith.ML Wed Nov 05 13:14:15 1997 +0100
@@ -125,7 +125,7 @@
by (safe_tac (claset() addSIs [sum_bij]));
(*Do the beta-reductions now*)
by (ALLGOALS (Asm_full_simp_tac));
-by (safe_tac (claset()));
+by Safe_tac;
(*8 subgoals!*)
by (ALLGOALS
(asm_full_simp_tac
@@ -141,7 +141,7 @@
lam_bijective 1);
by (blast_tac (claset() addSIs [if_type]) 2);
by (DEPTH_SOLVE_1 (eresolve_tac [case_type, UnI1, UnI2] 1));
-by (safe_tac (claset()));
+by Safe_tac;
by (ALLGOALS (asm_simp_tac (simpset() setloop split_tac [expand_if])));
by (blast_tac (claset() addEs [equalityE]) 1);
qed "sum_disjoint_bij";
@@ -249,7 +249,7 @@
\ (lam <x,y>:A*B. <f`x, g`y>) : bij(A*B, C*D)";
by (res_inst_tac [("d", "%<x,y>. <converse(f)`x, converse(g)`y>")]
lam_bijective 1);
-by (safe_tac (claset()));
+by Safe_tac;
by (ALLGOALS (asm_simp_tac bij_inverse_ss));
qed "prod_bij";
@@ -266,7 +266,7 @@
goal OrderArith.thy "(lam z:A. <x,z>) : bij(A, {x}*A)";
by (res_inst_tac [("d", "snd")] lam_bijective 1);
-by (safe_tac (claset()));
+by Safe_tac;
by (ALLGOALS Asm_simp_tac);
qed "singleton_prod_bij";
--- a/src/ZF/OrderType.ML Wed Nov 05 11:49:34 1997 +0100
+++ b/src/ZF/OrderType.ML Wed Nov 05 13:14:15 1997 +0100
@@ -103,13 +103,13 @@
goalw OrderType.thy [well_ord_def, tot_ord_def, part_ord_def]
"!!r. [| well_ord(A,r); x:A |] ==> Ord(ordermap(A,r) ` x)";
-by (safe_tac (claset()));
+by Safe_tac;
by (wf_on_ind_tac "x" [] 1);
by (asm_simp_tac (simpset() addsimps [ordermap_pred_unfold]) 1);
by (rtac (Ord_is_Transset RSN (2,OrdI)) 1);
by (rewrite_goals_tac [pred_def,Transset_def]);
by (Blast_tac 2);
-by (safe_tac (claset()));
+by Safe_tac;
by (ordermap_elim_tac 1);
by (fast_tac (claset() addSEs [trans_onD]) 1);
qed "Ord_ordermap";
@@ -120,7 +120,7 @@
by (rtac (Ord_is_Transset RSN (2,OrdI)) 1);
by (blast_tac (claset() addIs [Ord_ordermap]) 2);
by (rewrite_goals_tac [Transset_def,well_ord_def]);
-by (safe_tac (claset()));
+by Safe_tac;
by (ordermap_elim_tac 1);
by (Blast_tac 1);
qed "Ord_ordertype";
@@ -139,7 +139,7 @@
goalw OrderType.thy [well_ord_def, tot_ord_def]
"!!r. [| ordermap(A,r)`w : ordermap(A,r)`x; well_ord(A,r); \
\ w: A; x: A |] ==> <w,x>: r";
-by (safe_tac (claset()));
+by Safe_tac;
by (linear_case_tac 1);
by (blast_tac (claset() addSEs [mem_not_refl RS notE]) 1);
by (dtac ordermap_mono 1);
@@ -312,7 +312,7 @@
goal OrderType.thy "(lam z:A+0. case(%x. x, %y. y, z)) : bij(A+0, A)";
by (res_inst_tac [("d", "Inl")] lam_bijective 1);
-by (safe_tac (claset()));
+by Safe_tac;
by (ALLGOALS Asm_simp_tac);
qed "bij_sum_0";
@@ -325,7 +325,7 @@
goal OrderType.thy "(lam z:0+A. case(%x. x, %y. y, z)) : bij(0+A, A)";
by (res_inst_tac [("d", "Inr")] lam_bijective 1);
-by (safe_tac (claset()));
+by Safe_tac;
by (ALLGOALS Asm_simp_tac);
qed "bij_0_sum";
@@ -344,7 +344,7 @@
\ (lam x:pred(A,a,r). Inl(x)) \
\ : bij(pred(A,a,r), pred(A+B, Inl(a), radd(A,r,B,s)))";
by (res_inst_tac [("d", "case(%x. x, %y. y)")] lam_bijective 1);
-by (safe_tac (claset()));
+by Safe_tac;
by (ALLGOALS
(asm_full_simp_tac
(simpset() addsimps [radd_Inl_iff, radd_Inr_Inl_iff])));
@@ -364,7 +364,7 @@
\ id(A+pred(B,b,s)) \
\ : bij(A+pred(B,b,s), pred(A+B, Inr(b), radd(A,r,B,s)))";
by (res_inst_tac [("d", "%z. z")] lam_bijective 1);
-by (safe_tac (claset()));
+by Safe_tac;
by (ALLGOALS (Asm_full_simp_tac));
qed "pred_Inr_bij";
@@ -671,7 +671,7 @@
\ pred(A*B, <a,b>, rmult(A,r,B,s)) = \
\ pred(A,a,r)*B Un ({a} * pred(B,b,s))";
by (rtac equalityI 1);
-by (safe_tac (claset()));
+by Safe_tac;
by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [rmult_iff])));
by (ALLGOALS (Blast_tac));
qed "pred_Pair_eq";
@@ -703,7 +703,7 @@
by (REPEAT_FIRST (ares_tac [well_ord_rmult, well_ord_radd, well_ord_Memrel,
Ord_ordertype]));
by (ALLGOALS (asm_simp_tac (simpset() addsimps [Memrel_iff])));
-by (safe_tac (claset()));
+by Safe_tac;
by (ALLGOALS (blast_tac (claset() addIs [Ord_trans])));
qed "ordertype_pred_Pair_lemma";
--- a/src/ZF/Ordinal.ML Wed Nov 05 11:49:34 1997 +0100
+++ b/src/ZF/Ordinal.ML Wed Nov 05 13:14:15 1997 +0100
@@ -183,7 +183,7 @@
by (swap_res_tac [Ord_is_Transset RSN (2,OrdI)] 1);
by (Blast_tac 2);
by (rewtac Transset_def);
-by (safe_tac (claset()));
+by Safe_tac;
by (Asm_full_simp_tac 1);
by (REPEAT (eresolve_tac [asm_rl, Ord_in_Ord] 1));
qed "ON_class";
--- a/src/ZF/Perm.ML Wed Nov 05 11:49:34 1997 +0100
+++ b/src/ZF/Perm.ML Wed Nov 05 13:14:15 1997 +0100
@@ -44,7 +44,7 @@
(*Cantor's theorem revisited*)
goalw Perm.thy [surj_def] "f ~: surj(A,Pow(A))";
-by (safe_tac (claset()));
+by Safe_tac;
by (cut_facts_tac [cantor] 1);
by (fast_tac subset_cs 1);
qed "cantor_surj";
@@ -363,18 +363,18 @@
goalw Perm.thy [inj_def]
"!!f g. [| (f O g): inj(A,C); g: A->B; f: B->C |] ==> g: inj(A,B)";
-by (safe_tac (claset()));
+by Safe_tac;
by (REPEAT (eresolve_tac [asm_rl, bspec RS bspec RS mp] 1));
by (asm_simp_tac (simpset() ) 1);
qed "comp_mem_injD1";
goalw Perm.thy [inj_def,surj_def]
"!!f g. [| (f O g): inj(A,C); g: surj(A,B); f: B->C |] ==> f: inj(B,C)";
-by (safe_tac (claset()));
+by Safe_tac;
by (res_inst_tac [("x1", "x")] (bspec RS bexE) 1);
by (eres_inst_tac [("x1", "w")] (bspec RS bexE) 3);
by (REPEAT (assume_tac 1));
-by (safe_tac (claset()));
+by Safe_tac;
by (res_inst_tac [("t", "op `(g)")] subst_context 1);
by (REPEAT (eresolve_tac [asm_rl, bspec RS bspec RS mp] 1));
by (asm_simp_tac (simpset() ) 1);
@@ -392,7 +392,7 @@
goalw Perm.thy [inj_def,surj_def]
"!!f g. [| (f O g): surj(A,C); g: A->B; f: inj(B,C) |] ==> g: surj(A,B)";
-by (safe_tac (claset()));
+by Safe_tac;
by (eres_inst_tac [("x1", "f`y")] (bspec RS bexE) 1);
by (REPEAT (ares_tac [apply_type] 1 ORELSE dtac comp_fun_applyD 1));
by (blast_tac (claset() addSIs [apply_funtype]) 1);
@@ -426,7 +426,7 @@
goalw Perm.thy [id_def]
"!!f A B. [| f: A->B; g: B->A |] ==> \
\ f O g = id(B) <-> (ALL y:B. f`(g`y)=y)";
-by (safe_tac (claset()));
+by Safe_tac;
by (dres_inst_tac [("t", "%h. h`y ")] subst_context 1);
by (Asm_full_simp_tac 1);
by (rtac fun_extension 1);
--- a/src/ZF/Resid/Confluence.ML Wed Nov 05 11:49:34 1997 +0100
+++ b/src/ZF/Resid/Confluence.ML Wed Nov 05 13:14:15 1997 +0100
@@ -53,7 +53,7 @@
goalw Confluence.thy [confluence_def]
"!!u.[|confluence(Spar_red)|]==> confluence(Sred)";
-by(blast_tac (claset() addIs [par_red_red, red_par_red]) 1);
+by (blast_tac (claset() addIs [par_red_red, red_par_red]) 1);
val lemma1 = result();
bind_thm ("confluence_beta_reduction",
--- a/src/ZF/Resid/Cube.ML Wed Nov 05 11:49:34 1997 +0100
+++ b/src/ZF/Resid/Cube.ML Wed Nov 05 13:14:15 1997 +0100
@@ -34,7 +34,7 @@
goal Cube.thy
"!!u.[|v <== u; regular(u); w~v|]==> \
\ w |> u = (w|>v) |> (u|>v)";
-by (resolve_tac [prism_l] 1);
+by (rtac prism_l 1);
by (rtac comp_trans 4);
by (assume_tac 4);
by (ALLGOALS(asm_simp_tac prism_ss));
@@ -48,9 +48,9 @@
goal Cube.thy
"!!u.[|u~v; regular(v); regular(u); w~u|]==> \
\ (w|>u) |> (v|>u) = (w|>v) |> (u|>v)";
-by (rtac (preservation RS ssubst) 1
+by (stac preservation 1
THEN assume_tac 1 THEN assume_tac 1);
-by (rtac (preservation RS ssubst) 1
+by (stac preservation 1
THEN etac comp_sym 1 THEN assume_tac 1);
by (stac (prism RS sym) 1);
by (asm_full_simp_tac (simpset() addsimps
--- a/src/ZF/Resid/Reduction.ML Wed Nov 05 11:49:34 1997 +0100
+++ b/src/ZF/Resid/Reduction.ML Wed Nov 05 13:14:15 1997 +0100
@@ -31,7 +31,7 @@
[Spar_red.one_step, substL_type, redD1, redD2, par_redD1,
par_redD2, par_red1D2, unmark_type]);
-val reducL_ss = simpset() setloop (SELECT_GOAL (safe_tac (claset())));
+val reducL_ss = simpset() setloop (SELECT_GOAL Safe_tac);
(* ------------------------------------------------------------------------- *)
(* Lemmas for reduction *)
--- a/src/ZF/Resid/Residuals.ML Wed Nov 05 11:49:34 1997 +0100
+++ b/src/ZF/Resid/Residuals.ML Wed Nov 05 13:14:15 1997 +0100
@@ -100,11 +100,11 @@
by (etac Scomp.induct 1);
by (ALLGOALS (asm_full_simp_tac
(simpset() addsimps [res_Var,res_Fun,res_App,res_redex]
- setloop (SELECT_GOAL (safe_tac (claset()))))));
+ setloop (SELECT_GOAL Safe_tac))));
by (dres_inst_tac [("psi", "Fun(?u) |> ?v : redexes")] asm_rl 1);
by (asm_full_simp_tac
(simpset() addsimps [res_Fun]
- setloop (SELECT_GOAL (safe_tac (claset())))) 1);
+ setloop (SELECT_GOAL Safe_tac)) 1);
qed "resfunc_type";
Addsimps ([res_Var, res_Fun, res_App, res_redex, lift_rec_preserve_comp,
@@ -112,7 +112,7 @@
subst_rec_preserve_reg] @
redexes.free_iffs);
-val res1L_ss = simpset() setloop (SELECT_GOAL (safe_tac (claset())));
+val res1L_ss = simpset() setloop (SELECT_GOAL Safe_tac);
(* ------------------------------------------------------------------------- *)
(* Commutation theorem *)
@@ -178,7 +178,7 @@
goal Residuals.thy
"!!u. u~v ==> regular(u) --> regular(v) --> regular(u|>v)";
by (etac Scomp.induct 1);
-by (safe_tac (claset()));
+by Safe_tac;
by (TRYALL (dres_inst_tac [("psi", "regular(Fun(?u) |> ?v)")] asm_rl));
by (ALLGOALS (asm_full_simp_tac res1L_ss));
qed "residuals_preserve_reg";
@@ -196,7 +196,7 @@
goal Residuals.thy
"!!u. u ~ v ==> regular(v) --> u|>v = (u un v)|>v";
by (etac Scomp.induct 1);
-by (safe_tac (claset()));
+by Safe_tac;
by (dres_inst_tac [("psi", "Fun(?u) |> ?v = ?w")] asm_rl 3);
by (ALLGOALS (asm_full_simp_tac (res1L_ss addsimps
[union_preserve_comp,comp_sym_iff])));
--- a/src/ZF/Resid/SubUnion.ML Wed Nov 05 11:49:34 1997 +0100
+++ b/src/ZF/Resid/SubUnion.ML Wed Nov 05 13:14:15 1997 +0100
@@ -120,7 +120,7 @@
"!!u. u ~ v ==> regular(u)-->regular(v)-->regular(u un v)";
by (etac Scomp.induct 1);
by (ALLGOALS(asm_full_simp_tac
- (simpset() setloop(SELECT_GOAL (safe_tac (claset()))))));
+ (simpset() setloop(SELECT_GOAL Safe_tac))));
by (dres_inst_tac [("psi", "regular(Fun(?u) un ?v)")] asm_rl 1);
by (Asm_full_simp_tac 1);
qed_spec_mp "union_preserve_regular";
--- a/src/ZF/Univ.ML Wed Nov 05 11:49:34 1997 +0100
+++ b/src/ZF/Univ.ML Wed Nov 05 13:14:15 1997 +0100
@@ -93,13 +93,13 @@
goal Univ.thy "!!a. a: Vfrom(A,i) ==> {a} : Vfrom(A,succ(i))";
by (rtac subset_mem_Vfrom 1);
-by (safe_tac (claset()));
+by Safe_tac;
qed "singleton_in_Vfrom";
goal Univ.thy
"!!A. [| a: Vfrom(A,i); b: Vfrom(A,i) |] ==> {a,b} : Vfrom(A,succ(i))";
by (rtac subset_mem_Vfrom 1);
-by (safe_tac (claset()));
+by Safe_tac;
qed "doubleton_in_Vfrom";
goalw Univ.thy [Pair_def]
@@ -412,7 +412,7 @@
val [ordi] = goal Univ.thy "Ord(i) ==> ALL b. b : Vset(i) --> rank(b) < i";
by (rtac (ordi RS trans_induct) 1);
by (stac Vset 1);
-by (safe_tac (claset()));
+by Safe_tac;
by (stac rank 1);
by (rtac UN_succ_least_lt 1);
by (Blast_tac 2);
@@ -445,7 +445,7 @@
goal Univ.thy "!!i. Ord(i) ==> rank(Vset(i)) = i";
by (stac rank 1);
by (rtac equalityI 1);
-by (safe_tac (claset()));
+by Safe_tac;
by (EVERY' [rtac UN_I,
etac (i_subset_Vfrom RS subsetD),
etac (Ord_in_Ord RS rank_of_Ord RS ssubst),
@@ -633,7 +633,7 @@
"!!i. [| b: Fin(Vfrom(A,i)); Limit(i) |] ==> EX j. b <= Vfrom(A,j) & j<i";
by (etac Fin_induct 1);
by (blast_tac (claset() addSDs [Limit_has_0]) 1);
-by (safe_tac (claset()));
+by Safe_tac;
by (etac Limit_VfromE 1);
by (assume_tac 1);
by (blast_tac (claset() addSIs [Un_least_lt] addIs [Vfrom_UnI1, Vfrom_UnI2]) 1);
@@ -642,7 +642,7 @@
goal Univ.thy "!!i. Limit(i) ==> Fin(Vfrom(A,i)) <= Vfrom(A,i)";
by (rtac subsetI 1);
by (dtac Fin_Vfrom_lemma 1);
-by (safe_tac (claset()));
+by Safe_tac;
by (resolve_tac [Vfrom RS ssubst] 1);
by (blast_tac (claset() addSDs [ltD]) 1);
val Fin_VLimit = result();
--- a/src/ZF/Zorn.ML Wed Nov 05 11:49:34 1997 +0100
+++ b/src/ZF/Zorn.ML Wed Nov 05 13:14:15 1997 +0100
@@ -206,7 +206,7 @@
(*Now, verify that it increases*)
by (asm_simp_tac (simpset() addsimps [Pow_iff, subset_refl]
setloop split_tac [expand_if]) 1);
-by (safe_tac (claset()));
+by Safe_tac;
by (dtac choice_super 1);
by (REPEAT (assume_tac 1));
by (rewtac super_def);
@@ -228,7 +228,7 @@
setloop split_tac [expand_if]) 1);
by (rewtac chain_def);
by (rtac CollectI 1 THEN Blast_tac 1);
-by (safe_tac(claset()));
+by Safe_tac;
by (res_inst_tac [("m1","B"), ("n1","Ba")] (TFin_subset_linear RS disjE) 1);
by (ALLGOALS Fast_tac);
qed "TFin_chain_lemma4";
@@ -272,13 +272,13 @@
by (rename_tac "c" 1);
by (res_inst_tac [("x", "Union(c)")] bexI 1);
by (Blast_tac 2);
-by (safe_tac (claset()));
+by Safe_tac;
by (rename_tac "z" 1);
by (rtac classical 1);
by (subgoal_tac "cons(z,c): super(S,c)" 1);
by (blast_tac (claset() addEs [equalityE]) 1);
by (rewtac super_def);
-by (safe_tac (claset()));
+by Safe_tac;
by (fast_tac (claset() addEs [chain_extend]) 1);
by (blast_tac (claset() addEs [equalityE]) 1);
qed "Zorn";
--- a/src/ZF/ex/Integ.ML Wed Nov 05 11:49:34 1997 +0100
+++ b/src/ZF/ex/Integ.ML Wed Nov 05 13:14:15 1997 +0100
@@ -94,7 +94,7 @@
goalw Integ.thy [congruent_def]
"congruent(intrel, %<x,y>. intrel``{<y,x>})";
-by (safe_tac (claset()));
+by Safe_tac;
by (asm_full_simp_tac (simpset() addsimps add_ac) 1);
qed "zminus_congruent";
@@ -110,7 +110,7 @@
goalw Integ.thy [integ_def,zminus_def]
"!!z w. [| $~z = $~w; z: integ; w: integ |] ==> z=w";
by (etac (zminus_ize UN_equiv_class_inject) 1);
-by (safe_tac (claset()));
+by Safe_tac;
(*The setloop is only needed because assumptions are in the wrong order!*)
by (asm_full_simp_tac (simpset() addsimps add_ac
setloop dtac eq_intrelD) 1);
@@ -135,7 +135,7 @@
(*No natural number is negative!*)
goalw Integ.thy [znegative_def, znat_def] "~ znegative($# n)";
-by (safe_tac (claset()));
+by Safe_tac;
by (dres_inst_tac [("psi", "?lhs=?rhs")] asm_rl 1);
by (dres_inst_tac [("psi", "?lhs<?rhs")] asm_rl 1);
by (fast_tac (claset() addss
@@ -155,7 +155,7 @@
goalw Integ.thy [congruent_def]
"congruent(intrel, %<x,y>. (y#-x) #+ (x#-y))";
-by (safe_tac (claset()));
+by Safe_tac;
by (ALLGOALS Asm_simp_tac);
by (etac rev_mp 1);
by (res_inst_tac [("m","x1"),("n","y1")] diff_induct 1 THEN
@@ -209,7 +209,7 @@
\ let <x1,y1>=z1; <x2,y2>=z2 \
\ in intrel``{<x1#+x2, y1#+y2>})";
(*Proof via congruent2_commuteI seems longer*)
-by (safe_tac (claset()));
+by Safe_tac;
by (asm_simp_tac (simpset() addsimps [add_assoc, Let_def]) 1);
(*The rest should be trivial, but rearranging terms is hard;
add_ac does not help rewriting with the assumptions.*)
@@ -305,7 +305,7 @@
\ split(%x1 y1. split(%x2 y2. \
\ intrel``{<x1#*x2 #+ y1#*y2, x1#*y2 #+ y1#*x2>}, p2), p1))";
by (rtac (equiv_intrel RS congruent2_commuteI) 1);
-by (safe_tac (claset()));
+by Safe_tac;
by (ALLGOALS Asm_simp_tac);
(*Proof that zmult is congruent in one argument*)
by (asm_simp_tac
--- a/src/ZF/ex/LList.ML Wed Nov 05 11:49:34 1997 +0100
+++ b/src/ZF/ex/LList.ML Wed Nov 05 13:14:15 1997 +0100
@@ -77,7 +77,7 @@
by (REPEAT (resolve_tac [allI, impI] 1));
by (etac lleq.elim 1);
by (rewrite_goals_tac (QInr_def::llist.con_defs));
-by (safe_tac (claset()));
+by Safe_tac;
by (fast_tac (subset_cs addSEs [Ord_trans, make_elim bspec]) 1);
qed "lleq_Int_Vset_subset_lemma";
@@ -89,7 +89,7 @@
val [prem] = goal LList.thy "<l,l'> : lleq(A) ==> <l',l> : lleq(A)";
by (rtac (prem RS converseI RS lleq.coinduct) 1);
by (rtac (lleq.dom_subset RS converse_type) 1);
-by (safe_tac (claset()));
+by Safe_tac;
by (etac lleq.elim 1);
by (ALLGOALS Fast_tac);
qed "lleq_symmetric";
@@ -104,7 +104,7 @@
"[| l=l'; l: llist(A) |] ==> <l,l'> : lleq(A)";
by (res_inst_tac [("X", "{<l,l>. l: llist(A)}")] lleq.coinduct 1);
by (rtac (lprem RS RepFunI RS (eqprem RS subst)) 1);
-by (safe_tac (claset()));
+by Safe_tac;
by (etac llist.elim 1);
by (ALLGOALS Fast_tac);
qed "equal_llist_implies_leq";
--- a/src/ZF/ex/Limit.ML Wed Nov 05 11:49:34 1997 +0100
+++ b/src/ZF/ex/Limit.ML Wed Nov 05 13:14:15 1997 +0100
@@ -13,7 +13,7 @@
(* Useful goal commands. *)
(*----------------------------------------------------------------------*)
-val brr = fn thl => fn n => by(REPEAT(ares_tac thl n));
+val brr = fn thl => fn n => by (REPEAT(ares_tac thl n));
val trr = fn thl => fn n => (REPEAT(ares_tac thl n));
fun rotate n i = EVERY(replicate n (etac revcut_rl i));
@@ -70,7 +70,7 @@
\ rel(D,x,z); \
\ !!x y. [| rel(D,x,y); rel(D,y,x); x:set(D); y:set(D)|] ==> x=y |] ==> \
\ po(D)";
-by (safe_tac (claset()));
+by Safe_tac;
brr prems 1;
qed "poI";
@@ -139,19 +139,19 @@
val prems = goalw Limit.thy [islub_def] (* islubI *)
"[|isub(D,X,x); !!y. isub(D,X,y) ==> rel(D,x,y)|] ==> islub(D,X,x)";
-by (safe_tac (claset()));
+by Safe_tac;
by (REPEAT(ares_tac prems 1));
qed "islubI";
val prems = goalw Limit.thy [isub_def] (* isubI *)
"[|x:set(D); !!n. n:nat ==> rel(D,X`n,x)|] ==> isub(D,X,x)";
-by (safe_tac (claset()));
+by Safe_tac;
by (REPEAT(ares_tac prems 1));
qed "isubI";
val prems = goalw Limit.thy [isub_def] (* isubE *)
"!!z.[|isub(D,X,x);[|x:set(D); !!n. n:nat==>rel(D,X`n,x)|] ==> P|] ==> P";
-by (safe_tac (claset()));
+by Safe_tac;
by (Asm_simp_tac 1);
qed "isubE";
@@ -236,7 +236,7 @@
by (assume_tac 3);
by (rtac (hd prems) 2);
by (res_inst_tac [("n","m")] nat_induct 1);
-by (safe_tac (claset()));
+by Safe_tac;
by (asm_full_simp_tac (simpset() addsimps prems) 2);
by (rtac cpo_trans 4);
by (rtac (le_succ_eq RS subst) 3);
@@ -264,7 +264,7 @@
"pcpo(D) ==> EX! x. x:set(D) & (ALL y:set(D). rel(D,x,y))";
by (rtac (hd prems RS conjunct2 RS bexE) 1);
by (rtac ex1I 1);
-by (safe_tac (claset()));
+by Safe_tac;
by (assume_tac 1);
by (etac bspec 1);
by (assume_tac 1);
@@ -338,7 +338,7 @@
val prems = goalw Limit.thy [isub_def,suffix_def] (* isub_suffix *)
"[|chain(D,X); cpo(D); n:nat|] ==> isub(D,suffix(X,n),x) <-> isub(D,X,x)";
by (simp_tac (simpset() addsimps prems) 1);
-by (safe_tac (claset()));
+by Safe_tac;
by (dtac bspec 2);
by (assume_tac 3); (* to instantiate unknowns properly *)
by (rtac cpo_trans 1);
@@ -479,13 +479,13 @@
val prems = goalw Limit.thy [matrix_def] (* matrix_sym_axis *)
"!!z. matrix(D,M) ==> matrix(D,lam m:nat. lam n:nat. M`n`m)";
-by (Simp_tac 1 THEN safe_tac (claset()) THEN
+by (Simp_tac 1 THEN Safe_tac THEN
REPEAT(asm_simp_tac (simpset() addsimps [fun_swap]) 1));
qed "matrix_sym_axis";
val prems = goalw Limit.thy [chain_def] (* matrix_chain_diag *)
"matrix(D,M) ==> chain(D,lam n:nat. M`n`n)";
-by (safe_tac (claset()));
+by Safe_tac;
by (rtac lam_type 1);
by (rtac matrix_in 1);
by (REPEAT(ares_tac prems 1));
@@ -496,7 +496,7 @@
val prems = goalw Limit.thy [chain_def] (* matrix_chain_left *)
"[|matrix(D,M); n:nat|] ==> chain(D,M`n)";
-by (safe_tac (claset()));
+by Safe_tac;
by (rtac apply_type 1);
by (rtac matrix_fun 1);
by (REPEAT(ares_tac prems 1));
@@ -506,7 +506,7 @@
val prems = goalw Limit.thy [chain_def] (* matrix_chain_right *)
"[|matrix(D,M); m:nat|] ==> chain(D,lam n:nat. M`n`m)";
-by (safe_tac (claset()));
+by Safe_tac;
by (asm_simp_tac(simpset() addsimps prems) 2);
brr(lam_type::matrix_in::matrix_rel_1_0::prems) 1;
qed "matrix_chain_right";
@@ -537,7 +537,7 @@
"[|isub(D,(lam n:nat. M`n`n),y); matrix(D,M); cpo(D)|] ==> \
\ isub(D,(lam n:nat. lub(D,lam m:nat. M`n`m)),y)";
by (rewtac isub_def);
-by (safe_tac (claset()));
+by Safe_tac;
by (rtac isubD1 1);
by (resolve_tac prems 1);
by (Asm_simp_tac 1);
@@ -551,11 +551,11 @@
by (assume_tac 1);
by (resolve_tac prems 1);
by (rewtac isub_def);
-by (safe_tac (claset()));
+by Safe_tac;
by (rtac isubD1 1);
by (resolve_tac prems 1);
by (cut_inst_tac[("P","n le na")]excluded_middle 1);
-by (safe_tac (claset()));
+by Safe_tac;
by (rtac cpo_trans 1);
by (resolve_tac prems 1);
by (rtac (not_le_iff_lt RS iffD1 RS leI RS chain_rel_gen) 1);
@@ -575,7 +575,7 @@
val prems = goalw Limit.thy [chain_def] (* matrix_chain_lub *)
"[|matrix(D,M); cpo(D)|] ==> chain(D,lam n:nat. lub(D,lam m:nat. M`n`m))";
-by (safe_tac (claset()));
+by Safe_tac;
by (rtac lam_type 1);
by (rtac islub_in 1);
by (rtac cpo_lub 1);
@@ -722,7 +722,7 @@
"[|f:mono(D,E); chain(D,X)|] ==> chain(E,lam n:nat. f`(X`n))";
by (rewtac chain_def);
by (Simp_tac 1);
-by (safe_tac (claset()));
+by Safe_tac;
by (rtac lam_type 1);
by (rtac mono_map 1);
by (resolve_tac prems 1);
@@ -768,7 +768,7 @@
\ rel(cf(D,E),f,g)";
by (rtac rel_I 1);
by (simp_tac (simpset() addsimps [cf_def]) 1);
-by (safe_tac (claset()));
+by Safe_tac;
brr prems 1;
qed "rel_cfI";
@@ -1218,7 +1218,7 @@
val prems = goalw Limit.thy [projpair_def] (* projpair_id *)
"cpo(D) ==> projpair(D,D,id(set(D)),id(set(D)))";
-by (safe_tac (claset()));
+by Safe_tac;
brr(id_cont::id_comp::id_type::prems) 1;
by (stac id_comp 1); (* Matches almost anything *)
brr(id_cont::id_type::cpo_refl::cpo_cf::cont_cf::prems) 1;
@@ -1245,7 +1245,7 @@
val prems = goalw Limit.thy [projpair_def] (* lemma *)
"[|emb(D,D',e); emb(D',E,e'); cpo(D); cpo(D'); cpo(E)|] ==> \
\ projpair(D,E,e' O e,(Rp(D,D',e)) O (Rp(D',E,e')))";
-by (safe_tac (claset()));
+by Safe_tac;
brr(comp_pres_cont::Rp_cont::emb_cont::prems) 1;
by (rtac (comp_assoc RS subst) 1);
by (res_inst_tac[("t1","e'")](comp_assoc RS ssubst) 1);
@@ -1317,7 +1317,7 @@
\ g:(PROD n:nat. set(DD`n))|] ==> rel(iprod(DD),f,g)";
by (rtac rel_I 1);
by (Simp_tac 1);
-by (safe_tac (claset()));
+by Safe_tac;
brr prems 1;
qed "rel_iprodI";
@@ -1325,7 +1325,7 @@
"[|rel(iprod(DD),f,g); n:nat|] ==> rel(DD`n,f`n,g`n)";
by (cut_facts_tac[hd prems RS rel_E]1);
by (Asm_full_simp_tac 1);
-by (safe_tac (claset()));
+by Safe_tac;
by (etac bspec 1);
by (resolve_tac prems 1);
qed "rel_iprodE";
@@ -1336,7 +1336,7 @@
val prems = goalw Limit.thy [chain_def] (* chain_iprod *)
"[|chain(iprod(DD),X); !!n. n:nat ==> cpo(DD`n); n:nat|] ==> \
\ chain(DD`n,lam m:nat. X`m`n)";
-by (safe_tac (claset()));
+by Safe_tac;
by (rtac lam_type 1);
by (rtac apply_type 1);
by (rtac iprodE 1);
@@ -1351,7 +1351,7 @@
val prems = goalw Limit.thy [islub_def,isub_def] (* islub_iprod *)
"[|chain(iprod(DD),X); !!n. n:nat ==> cpo(DD`n)|] ==> \
\ islub(iprod(DD),X,lam n:nat. lub(DD`n,lam m:nat. X`m`n))";
-by (safe_tac (claset()));
+by Safe_tac;
by (rtac iprodI 1);
by (rtac lam_type 1);
brr((chain_iprod RS cpo_lub RS islub_in)::prems) 1;
@@ -1366,7 +1366,7 @@
by (Asm_simp_tac 1);
brr(islub_least::(chain_iprod RS cpo_lub)::prems) 1;
by (rewtac isub_def);
-by (safe_tac (claset()));
+by Safe_tac;
by (etac (iprodE RS apply_type) 1);
by (assume_tac 1);
by (Asm_simp_tac 1);
@@ -1403,7 +1403,7 @@
"[|set(D)<=set(E); \
\ !!x y. [|x:set(D); y:set(D)|] ==> rel(D,x,y)<->rel(E,x,y); \
\ !!X. chain(D,X) ==> lub(E,X) : set(D)|] ==> subcpo(D,E)";
-by (safe_tac (claset()));
+by Safe_tac;
by (asm_full_simp_tac(simpset() addsimps prems) 2);
by (asm_simp_tac(simpset() addsimps prems) 2);
brr(prems@[subsetD]) 1;
@@ -1564,7 +1564,7 @@
val prems = goalw Limit.thy [emb_chain_def] (* emb_chainI *)
"[|!!n. n:nat ==> cpo(DD`n); \
\ !!n. n:nat ==> emb(DD`n,DD`succ(n),ee`n)|] ==> emb_chain(DD,ee)";
-by (safe_tac (claset()));
+by Safe_tac;
brr prems 1;
qed "emb_chainI";
@@ -1702,7 +1702,7 @@
by (res_inst_tac[("n","x")]nat_induct 1);
by (resolve_tac prems 1);
by (Fast_tac 1);
-by (safe_tac (claset()));
+by Safe_tac;
by (Asm_simp_tac 1);
by (Asm_simp_tac 1);
qed "succ_sub1";
@@ -1713,7 +1713,7 @@
by (resolve_tac prems 1);
by (rtac impI 1);
by (asm_full_simp_tac(simpset() addsimps prems) 1);
-by (safe_tac (claset()));
+by Safe_tac;
by (asm_full_simp_tac(simpset() addsimps prems) 1); (* Surprise, surprise. *)
qed "succ_le_pos";
@@ -1721,7 +1721,7 @@
"!!z. [|n:nat; m:nat|] ==> m le n --> (EX k:nat. n = m #+ k)";
by (res_inst_tac[("n","m")]nat_induct 1);
by (assume_tac 1);
-by (safe_tac (claset()));
+by Safe_tac;
by (rtac bexI 1);
by (rtac (add_0 RS sym) 1);
by (assume_tac 1);
@@ -1828,7 +1828,7 @@
brr(add_le_mono::nat_le_refl::add_type::nat_succI::prems) 1;
by (stac comp_assoc 1);
brr(comp_mono_eq::refl::[]) 1;
-(* by(asm_simp_tac ZF_ss 1); *)
+(* by (asm_simp_tac ZF_ss 1); *)
by (asm_simp_tac(ZF_ss addsimps(e_less_eq::add_type::nat_succI::prems)) 1);
by (stac id_comp 1); (* simp cannot unify/inst right, use brr below(?). *)
brr((emb_e_less_add RS emb_cont RS cont_fun)::refl::nat_succI::prems) 1;
@@ -2012,7 +2012,7 @@
by (stac id_comp 1);
brr((e_less_cont RS cont_fun)::add_type::add_le_mono::nat_le_refl::refl::
prems) 1;
-by(asm_full_simp_tac(ZF_ss addsimps(e_less_eq::nat_succI::add_type::prems)) 1);
+by (asm_full_simp_tac(ZF_ss addsimps(e_less_eq::nat_succI::add_type::prems)) 1);
by (stac comp_id 1);
brr((e_gr_cont RS cont_fun)::add_type::nat_succI::add_le_self::refl::prems) 1;
qed "e_gr_e_less_split_add";
@@ -2029,7 +2029,7 @@
"[|emb_chain(DD,ee); m:nat; n:nat|] ==> \
\ eps(DD,ee,m,n): set(DD`m)->set(DD`n)";
by (rtac (expand_if RS iffD2) 1);
-by (safe_tac (claset()));
+by Safe_tac;
brr((e_less_cont RS cont_fun)::prems) 1;
brr((not_le_iff_lt RS iffD1 RS leI)::e_gr_fun::nat_into_Ord::prems) 1;
qed "eps_fun";
@@ -2051,7 +2051,7 @@
val prems = goalw Limit.thy [eps_def] (* eps_e_gr_add *)
"[|n:nat; k:nat|] ==> eps(DD,ee,n#+k,n) = e_gr(DD,ee,n#+k,n)";
by (rtac (expand_if RS iffD2) 1);
-by (safe_tac (claset()));
+by Safe_tac;
by (etac leE 1);
(* Must control rewriting by instantiating a variable. *)
by (asm_full_simp_tac(simpset() addsimps
@@ -2433,7 +2433,7 @@
"[| !!n. n:nat ==> emb(DD`n,E,r(n)); \
\ !!m n. [|m le n; m:nat; n:nat|] ==> r(n) O eps(DD,ee,m,n) = r(m) |] ==> \
\ commute(DD,ee,E,r)";
-by (safe_tac (claset()));
+by Safe_tac;
brr prems 1;
qed "commuteI";
@@ -2663,7 +2663,7 @@
\ (E,G, \
\ lub(cf(E,G), lam n:nat. f(n) O Rp(DD`n,E,r(n))), \
\ lub(cf(G,E), lam n:nat. r(n) O Rp(DD`n,G,f(n))))";
-by (safe_tac (claset()));
+by Safe_tac;
by (stac comp_lubs 3);
(* The following one line is 15 lines in HOL, and includes existentials. *)
brr(cf_cont::islub_in::cpo_lub::cpo_cf::theta_chain::theta_proj_chain::prems) 1;
@@ -2759,7 +2759,7 @@
val mediatingI = prove_goalw Limit.thy [mediating_def]
"[|emb(E,G,t); !!n. n:nat ==> f(n) = t O r(n) |]==>mediating(E,G,r,f,t)"
- (fn prems => [safe_tac (claset()),trr prems 1]);
+ (fn prems => [Safe_tac,trr prems 1]);
val mediating_emb = prove_goalw Limit.thy [mediating_def]
"!!z. mediating(E,G,r,f,t) ==> emb(E,G,t)"
@@ -2816,7 +2816,7 @@
\ (ALL t. mediating(Dinf(DD,ee),G,rho_emb(DD,ee),f,t) --> \
\ t = lub(cf(Dinf(DD,ee),G), \
\ lam n:nat. f(n) O Rp(DD`n,Dinf(DD,ee),rho_emb(DD,ee,n))))";
-by (safe_tac (claset()));
+by Safe_tac;
brr(lub_universal_mediating::rho_emb_commute::rho_emb_lub::cpo_Dinf::prems) 1;
brr(lub_universal_unique::rho_emb_commute::rho_emb_lub::cpo_Dinf::prems) 1;
qed "Dinf_universal";
--- a/src/ZF/ex/Mutil.ML Wed Nov 05 11:49:34 1997 +0100
+++ b/src/ZF/ex/Mutil.ML Wed Nov 05 13:14:15 1997 +0100
@@ -76,7 +76,7 @@
goal thy "!!t. t:tiling(domino) ==> Finite(t)";
by (eresolve_tac [tiling.induct] 1);
-by (resolve_tac [Finite_0] 1);
+by (rtac Finite_0 1);
by (blast_tac (claset() addSIs [Finite_Un] addIs [domino_Finite]) 1);
qed "tiling_domino_Finite";
@@ -121,8 +121,8 @@
\ t = (succ(m)#+succ(m))*(succ(n)#+succ(n)); \
\ t' = t - {<0,0>} - {<succ(m#+m), succ(n#+n)>} |] ==> \
\ t' ~: tiling(domino)";
-by (resolve_tac [notI] 1);
-by (dresolve_tac [tiling_domino_0_1] 1);
+by (rtac notI 1);
+by (dtac tiling_domino_0_1 1);
by (subgoal_tac "|evnodd(t',0)| < |evnodd(t',1)|" 1);
by (asm_full_simp_tac (simpset() addsimps [lt_not_refl]) 1);
by (subgoal_tac "t : tiling(domino)" 1);
@@ -134,7 +134,7 @@
by (asm_full_simp_tac
(simpset() addsimps [evnodd_Diff, mod2_add_self,
mod2_succ_succ, tiling_domino_0_1 RS sym]) 1);
-by (resolve_tac [lt_trans] 1);
+by (rtac lt_trans 1);
by (REPEAT
(rtac Finite_imp_cardinal_Diff 1
THEN
--- a/src/ZF/ex/Ntree.ML Wed Nov 05 11:49:34 1997 +0100
+++ b/src/ZF/ex/Ntree.ML Wed Nov 05 13:14:15 1997 +0100
@@ -58,7 +58,7 @@
goalw Ntree.thy (ntree.defs@ntree.con_defs) "ntree(univ(A)) <= univ(A)";
by (rtac lfp_lowerbound 1);
by (rtac (A_subset_univ RS univ_mono) 2);
-by (safe_tac (claset()));
+by Safe_tac;
by (REPEAT (ares_tac [Pair_in_univ, nat_fun_univ RS subsetD] 1));
qed "ntree_univ";
--- a/src/ZF/ex/Primes.ML Wed Nov 05 11:49:34 1997 +0100
+++ b/src/ZF/ex/Primes.ML Wed Nov 05 13:14:15 1997 +0100
@@ -150,7 +150,7 @@
by (asm_simp_tac (simpset() addsimps [egcd_0,dvd_refl,dvd_0_right,
dvd_imp_nat2]) 2);
(* case x > 0 *)
-by (safe_tac (claset()));
+by Safe_tac;
by (asm_simp_tac (simpset() addsimps [egcd_lt_0, nat_into_Ord RS Ord_0_lt,
dvd_imp_nat2]) 1);
by (eres_inst_tac [("x","a mod x")] ballE 1);
--- a/src/ZF/ex/Primrec.ML Wed Nov 05 11:49:34 1997 +0100
+++ b/src/ZF/ex/Primrec.ML Wed Nov 05 13:14:15 1997 +0100
@@ -273,7 +273,7 @@
by (DO_GOAL [res_inst_tac [("x","0")] bexI,
asm_simp_tac (simpset() addsimps [lt_ack1, nat_0_le]),
resolve_tac nat_typechecks] 1);
-by (safe_tac (claset()));
+by Safe_tac;
by (Asm_simp_tac 1);
by (rtac (ballI RS bexI) 1);
by (rtac (add_lt_mono RS lt_trans) 1);
@@ -352,7 +352,7 @@
goal Primrec.thy
"!!f. f:primrec ==> EX k:nat. ALL l:list(nat). f`l < ack(k, list_add(l))";
by (etac primrec.induct 1);
-by (safe_tac (claset()));
+by Safe_tac;
by (DEPTH_SOLVE
(ares_tac ([SC_case, CONST_case, PROJ_case, COMP_case, PREC_case,
bexI, ballI] @ nat_typechecks) 1));
--- a/src/ZF/ex/PropLog.ML Wed Nov 05 11:49:34 1997 +0100
+++ b/src/ZF/ex/PropLog.ML Wed Nov 05 13:14:15 1997 +0100
@@ -263,7 +263,7 @@
"[| p: prop; 0 |= p |] ==> ALL t. hyps(p,t) - hyps(p,t0) |- p";
by (rtac (premp RS hyps_finite RS Fin_induct) 1);
by (simp_tac (simpset() addsimps [premp, sat, logcon_thms_p, Diff_0]) 1);
-by (safe_tac (claset()));
+by Safe_tac;
(*Case hyps(p,t)-cons(#v,Y) |- p *)
by (rtac thms_excluded_middle_rule 1);
by (etac prop.Var_I 3);
--- a/src/ZF/ex/Ramsey.ML Wed Nov 05 11:49:34 1997 +0100
+++ b/src/ZF/ex/Ramsey.ML Wed Nov 05 13:14:15 1997 +0100
@@ -88,7 +88,7 @@
by (nat_ind_tac "n" [] 1);
by (fast_tac (claset() addSIs [Atleast0]) 1);
by (asm_simp_tac (simpset() addsimps [add_succ_right]) 1);
-by (safe_tac (claset()));
+by Safe_tac;
by (etac (Atleast_succD RS bexE) 1);
by (etac UnE 1);
(**case x:B. Instantiate the 'ALL A B' induction hypothesis. **)
@@ -165,7 +165,7 @@
"[| Ramsey(succ(m), succ(i), j); Ramsey(n, i, succ(j)); \
\ m: nat; n: nat |] ==> \
\ Ramsey(succ(m#+n), succ(i), succ(j))";
-by (safe_tac (claset()));
+by Safe_tac;
by (etac (Atleast_succD RS bexE) 1);
by (eres_inst_tac [("P1","%z.<x,z>:E")] (Atleast_partition RS disjE) 1);
by (REPEAT (resolve_tac prems 1));
@@ -173,13 +173,13 @@
by (rtac (ram1 RS spec RS spec RS mp RS disjE) 1);
by (Fast_tac 1);
by (fast_tac (claset() addEs [Clique_superset]) 1); (*easy -- given a Clique*)
-by (safe_tac (claset()));
+by Safe_tac;
by (eresolve_tac (swapify [exI]) 1); (*ignore main EX quantifier*)
by (REPEAT (ares_tac [Indept_succ] 1)); (*make a bigger Indept*)
(*case n*)
by (rtac (ram2 RS spec RS spec RS mp RS disjE) 1);
by (Fast_tac 1);
-by (safe_tac (claset()));
+by Safe_tac;
by (rtac exI 1);
by (REPEAT (ares_tac [Clique_succ] 1)); (*make a bigger Clique*)
by (fast_tac (claset() addEs [Indept_superset]) 1); (*easy -- given an Indept*)
--- a/src/ZF/ex/Term.ML Wed Nov 05 11:49:34 1997 +0100
+++ b/src/ZF/ex/Term.ML Wed Nov 05 13:14:15 1997 +0100
@@ -51,7 +51,7 @@
goalw Term.thy (term.defs@term.con_defs) "term(univ(A)) <= univ(A)";
by (rtac lfp_lowerbound 1);
by (rtac (A_subset_univ RS univ_mono) 2);
-by (safe_tac (claset()));
+by Safe_tac;
by (REPEAT (ares_tac [Pair_in_univ, list_univ RS subsetD] 1));
qed "term_univ";
--- a/src/ZF/ex/misc.ML Wed Nov 05 11:49:34 1997 +0100
+++ b/src/ZF/ex/misc.ML Wed Nov 05 13:14:15 1997 +0100
@@ -45,7 +45,7 @@
\ (ALL x:A. ALL y:A. H`(f`<x,y>) = g`<H`x,H`y>)}) --> \
\ J : hom(A,f,B,g) & K : hom(B,g,C,h) --> \
\ (K O J) : hom(A,f,C,h)";
-by (asm_simp_tac (simpset() setloop (K (safe_tac (claset())))) 1);
+by (asm_simp_tac (simpset() setloop (K Safe_tac)) 1);
val comp_homs = result();
(*This version uses meta-level rewriting, safe_tac and asm_simp_tac*)
@@ -56,7 +56,7 @@
\ J : hom(A,f,B,g) & K : hom(B,g,C,h) --> \
\ (K O J) : hom(A,f,C,h)";
by (rewtac hom_def);
-by (safe_tac (claset()));
+by Safe_tac;
by (Asm_simp_tac 1);
by (Asm_simp_tac 1);
qed "comp_homs";