--- a/src/HOL/Arith.ML Mon Sep 29 11:36:44 1997 +0200
+++ b/src/HOL/Arith.ML Mon Sep 29 11:37:02 1997 +0200
@@ -403,7 +403,7 @@
Addsimps [diff_add_inverse2];
goal Arith.thy "!!i j k::nat. i<=j ==> (j-i=k) = (j=k+i)";
-by (Step_tac 1);
+by Safe_tac;
by (ALLGOALS Asm_simp_tac);
qed "le_imp_diff_is_add";
@@ -546,7 +546,7 @@
goal Arith.thy "!!k. 0<k ==> (m*k = n*k) = (m=n)";
by (cut_facts_tac [less_linear] 1);
-by (Step_tac 1);
+by Safe_tac;
by (assume_tac 2);
by (ALLGOALS (dtac mult_less_mono1 THEN' assume_tac));
by (ALLGOALS Asm_full_simp_tac);
--- a/src/HOL/Divides.ML Mon Sep 29 11:36:44 1997 +0200
+++ b/src/HOL/Divides.ML Mon Sep 29 11:37:02 1997 +0200
@@ -229,7 +229,7 @@
goal thy "Suc(Suc(m)) mod 2 = m mod 2";
by (subgoal_tac "m mod 2 < 2" 1);
by (asm_simp_tac (!simpset addsimps [mod_less_divisor]) 2);
-by (Step_tac 1);
+by Safe_tac;
by (ALLGOALS (asm_simp_tac (!simpset addsimps [mod_Suc])));
qed "mod2_Suc_Suc";
Addsimps [mod2_Suc_Suc];
@@ -390,7 +390,7 @@
qed "dvd_imp_le";
goalw thy [dvd_def] "!!k. 0<k ==> (k dvd n) = (n mod k = 0)";
-by (Step_tac 1);
+by Safe_tac;
by (stac mult_commute 1);
by (Asm_simp_tac 1);
by (eres_inst_tac [("t","n")] (mod_div_equality RS subst) 1);
--- a/src/HOL/Finite.ML Mon Sep 29 11:36:44 1997 +0200
+++ b/src/HOL/Finite.ML Mon Sep 29 11:37:02 1997 +0200
@@ -378,7 +378,7 @@
goal Finite.thy "!!A. finite(A) ==> inj_onto f A --> card (f `` A) = card A";
by (etac finite_induct 1);
by (ALLGOALS Asm_simp_tac);
-by (Step_tac 1);
+by Safe_tac;
by (rewtac inj_onto_def);
by (Blast_tac 1);
by (stac card_insert_disjoint 1);
--- a/src/HOL/Induct/Comb.ML Mon Sep 29 11:36:44 1997 +0200
+++ b/src/HOL/Induct/Comb.ML Mon Sep 29 11:37:02 1997 +0200
@@ -130,7 +130,7 @@
goalw Comb.thy [diamond_def] "diamond parcontract";
by (rtac (impI RS allI RS allI) 1);
by (etac parcontract.induct 1 THEN prune_params_tac);
-by (Step_tac 1);
+by Safe_tac;
by (ALLGOALS Blast_tac);
qed "diamond_parcontract";
--- a/src/HOL/Induct/LFilter.ML Mon Sep 29 11:36:44 1997 +0200
+++ b/src/HOL/Induct/LFilter.ML Mon Sep 29 11:37:02 1997 +0200
@@ -187,7 +187,7 @@
goal thy "lfilter p (lfilter p l) = lfilter p l";
by (res_inst_tac [("l","l")] llist_fun_equalityI 1);
by (ALLGOALS (simp_tac (!simpset setloop split_tac[expand_if])));
-by (Step_tac 1);
+by Safe_tac;
(*Cases: p x is true or false*)
by (Blast_tac 1);
by (rtac (lfilter_cases RS disjE) 1);
@@ -327,7 +327,7 @@
goal thy "lfilter p (lmap f l) = lmap f (lfilter (p o f) l)";
by (res_inst_tac [("l","l")] llist_fun_equalityI 1);
by (ALLGOALS (simp_tac (!simpset setloop split_tac[expand_if])));
-by (Step_tac 1);
+by Safe_tac;
by (Blast_tac 1);
by (case_tac "lmap f l : Domain (findRel p)" 1);
by (subgoal_tac "l ~: Domain (findRel(%x. p (f x)))" 2);
--- a/src/HOL/Induct/PropLog.ML Mon Sep 29 11:36:44 1997 +0200
+++ b/src/HOL/Induct/PropLog.ML Mon Sep 29 11:37:02 1997 +0200
@@ -186,7 +186,7 @@
"{} |= p ==> !t. hyps p t - hyps p t0 |- p";
by (rtac (hyps_subset RS (hyps_finite RS finite_subset_induct)) 1);
by (simp_tac (!simpset addsimps [sat RS sat_thms_p]) 1);
-by (Step_tac 1);
+by Safe_tac;
(*Case hyps(p,t)-insert(#v,Y) |- p *)
by (rtac thms_excluded_middle_rule 1);
by (rtac (insert_Diff_same RS weaken_left) 1);
--- a/src/HOL/MiniML/MiniML.ML Mon Sep 29 11:36:44 1997 +0200
+++ b/src/HOL/MiniML/MiniML.ML Mon Sep 29 11:37:02 1997 +0200
@@ -125,7 +125,7 @@
Addsimps [aux_plus];
goal thy "!!t::typ. new_tv n t ==> {x. ? y. x = n + y} Int free_tv t = {}";
-by (step_tac (!claset) 1);
+by Safe_tac;
by (cut_facts_tac [aux_plus] 1);
by (dtac new_tv_le 1);
by (assume_tac 1);
@@ -135,7 +135,7 @@
val new_tv_Int_free_tv_empty_type = result ();
goal thy "!!sch::type_scheme. new_tv n sch ==> {x. ? y. x = n + y} Int free_tv sch = {}";
-by (step_tac (!claset) 1);
+by Safe_tac;
by (cut_facts_tac [aux_plus] 1);
by (dtac new_tv_le 1);
by (assume_tac 1);
--- a/src/HOL/Subst/Subst.ML Mon Sep 29 11:36:44 1997 +0200
+++ b/src/HOL/Subst/Subst.ML Mon Sep 29 11:37:02 1997 +0200
@@ -181,7 +181,7 @@
by (induct_tac "t" 1);
by (ALLGOALS (asm_full_simp_tac (!simpset addsimps [sdom_iff,srange_iff])));
by (Blast_tac 2);
-by (REPEAT (step_tac (!claset addIs [vars_var_iff RS iffD1 RS sym]) 1));
+by (safe_tac (!claset addSIs [exI, vars_var_iff RS iffD1 RS sym]));
by (Auto_tac());
qed_spec_mp "Var_intro";
--- a/src/HOL/Subst/Unifier.ML Mon Sep 29 11:36:44 1997 +0200
+++ b/src/HOL/Subst/Unifier.ML Mon Sep 29 11:37:02 1997 +0200
@@ -55,7 +55,7 @@
"!!v. ~ Var v <: t ==> MGUnifier [(v,t)] (Var v) t";
by (simp_tac(!simpset addsimps [MGU_iff, Unifier_def, MoreGeneral_def]
delsimps [subst_Var]) 1);
-by (Step_tac 1);
+by Safe_tac;
by (rtac exI 1);
by (etac subst 1 THEN rtac (Cons_trivial RS subst_sym) 1);
by (etac ssubst_subst2 1);
--- a/src/HOL/Subst/Unify.ML Mon Sep 29 11:36:44 1997 +0200
+++ b/src/HOL/Subst/Unify.ML Mon Sep 29 11:37:02 1997 +0200
@@ -44,7 +44,7 @@
wf_inv_image, wf_lex_prod, wf_finite_psubset,
wf_measure]) 1);
(* TC *)
-by (Step_tac 1);
+by Safe_tac;
by (simp_tac (!simpset addsimps [finite_psubset_def, finite_vars_of,
lex_prod_def, measure_def, inv_image_def]) 1);
by (rtac (monotone_vars_of RS (subset_iff_psubset_eq RS iffD1) RS disjE) 1);
--- a/src/HOL/equalities.ML Mon Sep 29 11:36:44 1997 +0200
+++ b/src/HOL/equalities.ML Mon Sep 29 11:37:02 1997 +0200
@@ -634,7 +634,7 @@
Addsimps [Pow_empty];
goal Set.thy "Pow (insert a A) = Pow A Un (insert a `` Pow A)";
-by (Step_tac 1);
+by Safe_tac;
by (etac swap 1);
by (res_inst_tac [("x", "x-{a}")] image_eqI 1);
by (ALLGOALS Blast_tac);
--- a/src/HOL/ex/Fib.ML Mon Sep 29 11:36:44 1997 +0200
+++ b/src/HOL/ex/Fib.ML Mon Sep 29 11:37:02 1997 +0200
@@ -54,7 +54,7 @@
(asm_simp_tac (!simpset addsimps [add_mult_distrib, add_mult_distrib2,
mod_less, mod_Suc]
setloop split_tac[expand_if])));
-by (step_tac (!claset addSDs [mod2_neq_0]) 1);
+by (safe_tac (!claset addSDs [mod2_neq_0]));
by (ALLGOALS
(asm_full_simp_tac
(!simpset addsimps (fib.rules @ add_ac @ mult_ac @
--- a/src/HOLCF/Porder.ML Mon Sep 29 11:36:44 1997 +0200
+++ b/src/HOLCF/Porder.ML Mon Sep 29 11:37:02 1997 +0200
@@ -68,7 +68,7 @@
"!!F. is_chain(F) ==> is_tord(range(F))"
(fn _ =>
[
- (Step_tac 1),
+ Safe_tac,
(rtac nat_less_cases 1),
(ALLGOALS (fast_tac (!claset addIs [refl_less, chain_mono RS mp])))]);