--- a/src/HOL/MiniML/MiniML.ML Tue Apr 22 11:37:12 1997 +0200
+++ b/src/HOL/MiniML/MiniML.ML Tue Apr 22 11:45:22 1997 +0200
@@ -74,8 +74,8 @@
\ else TVar x) o \
\ (%x. if x : free_tv A \
\ then x else n + x)) A)";
-by (rtac (S_o_alpha_type_scheme_list RS ssubst) 1);
-by (rtac (alpha_A RS ssubst) 1);
+by (stac S_o_alpha_type_scheme_list 1);
+by (stac alpha_A 1);
by (rtac refl 1);
qed "S'_A_eq_S'_alpha_A";
--- a/src/HOL/MiniML/Type.ML Tue Apr 22 11:37:12 1997 +0200
+++ b/src/HOL/MiniML/Type.ML Tue Apr 22 11:45:22 1997 +0200
@@ -318,9 +318,9 @@
"free_tv (%u::nat. $ s1 (s2 u) :: typ) <= \
\ free_tv s1 Un free_tv s2";
by (fast_tac (set_cs addSDs [free_tv_app_subst_te RS subsetD,
- free_tv_subst_var RS subsetD]
- addss (!simpset delsimps bex_simps
- addsimps [cod_def,dom_def])) 1);
+ free_tv_subst_var RS subsetD]
+ addss (!simpset delsimps bex_simps
+ addsimps [cod_def,dom_def])) 1);
qed "free_tv_comp_subst";
goalw thy [o_def]
@@ -481,7 +481,7 @@
goal thy "new_tv n S --> new_tv n (sch::type_scheme) --> new_tv n ($ S sch)";
by (type_scheme.induct_tac "sch" 1);
by (ALLGOALS (Asm_full_simp_tac));
-by (rewrite_goals_tac [new_tv_def]);
+by (rewtac new_tv_def);
by (simp_tac (!simpset addsimps [free_tv_subst,dom_def,cod_def]) 1);
by (strip_tac 1);
by (case_tac "S nat = TVar nat" 1);
@@ -638,7 +638,7 @@
by (REPEAT (etac exE 1));
by (rename_tac "n2 n1" 1);
by (res_inst_tac [("x","(max n1 n2)")] exI 1);
-by (rewrite_goals_tac [new_tv_def]);
+by (rewtac new_tv_def);
by (fast_tac (!claset addIs [less_maxL,less_maxR]) 1);
qed "ex_fresh_variable";
--- a/src/HOL/MiniML/W.ML Tue Apr 22 11:37:12 1997 +0200
+++ b/src/HOL/MiniML/W.ML Tue Apr 22 11:45:22 1997 +0200
@@ -206,13 +206,13 @@
ba 1;
ba 1;
ba 1;
-by (rewrite_goals_tac [new_tv_def]);
+by (rewtac new_tv_def);
by (Asm_simp_tac 1);
by (dtac W_var_ge 1);
by (rtac allI 1);
by (rename_tac "p" 1);
by (strip_tac 1);
-by (rewrite_goals_tac [free_tv_subst]);
+by (rewtac free_tv_subst);
by (dtac (free_tv_app_subst_scheme_list RS subsetD) 1);
fun restrict_prems is tacf =
METAHYPS(fn prems =>
@@ -494,7 +494,7 @@
by (eres_inst_tac [("x","Suc n")] allE 1);
by (best_tac (HOL_cs addSDs [mk_scheme_injective]
unsafe_addss (!simpset addcongs [conj_cong]
- setloop (split_tac [expand_option_bind]))) 1);
+ setloop (split_tac [expand_option_bind]))) 1);
(** LEVEL 19 **)
(* case App e1 e2 *)
--- a/src/HOL/W0/W.ML Tue Apr 22 11:37:12 1997 +0200
+++ b/src/HOL/W0/W.ML Tue Apr 22 11:45:22 1997 +0200
@@ -174,7 +174,7 @@
by (eres_inst_tac [("x","na")] allE 1);
by (eres_inst_tac [("x","v")] allE 1);
by (fast_tac (HOL_cs addSEs [allE]
- addIs [cod_app_subst]
+ addIs [cod_app_subst]
addss (!simpset addsimps [less_Suc_eq])) 1);
(** LEVEL 12 **)
(* case App e1 e2 *)
@@ -211,11 +211,11 @@
by (dtac (sym RS W_var_geD) 1);
by ( (forward_tac [less_le_trans] 1) THEN (assume_tac 1) );
by (fast_tac (HOL_cs addDs [mgu_free, codD,free_tv_subst_var RS subsetD,
- free_tv_app_subst_te RS subsetD,
- free_tv_app_subst_tel RS subsetD,
- less_le_trans,subsetD]
- addSEs [UnE]
- addss !simpset) 1);
+ free_tv_app_subst_te RS subsetD,
+ free_tv_app_subst_tel RS subsetD,
+ less_le_trans,subsetD]
+ addSEs [UnE]
+ addss !simpset) 1);
qed_spec_mp "free_tv_W";
(* Completeness of W w.r.t. has_type *)
@@ -370,7 +370,7 @@
by (asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
by (dtac (free_tv_app_subst_tel RS subsetD) 1);
by (fast_tac (set_cs addDs [codD,subst_comp_tel RSN (2,trans),
- eq_subst_tel_eq_free]
+ eq_subst_tel_eq_free]
addss ((!simpset addsimps [free_tv_subst,dom_def]))) 1);
(** LEVEL 106 **)
by (Fast_tac 1);