--- a/src/HOLCF/ex/Loop.ML Thu Sep 26 12:50:48 1996 +0200
+++ b/src/HOLCF/ex/Loop.ML Thu Sep 26 15:14:23 1996 +0200
@@ -47,15 +47,15 @@
(simp_tac HOLCF_ss 1),
(rtac allI 1),
(rtac trans 1),
- (rtac (while_unfold RS ssubst) 1),
+ (stac while_unfold 1),
(rtac refl 2),
- (rtac (iterate_Suc2 RS ssubst) 1),
+ (stac iterate_Suc2 1),
(rtac trans 1),
(etac spec 2),
- (rtac (step_def2 RS ssubst) 1),
+ (stac step_def2 1),
(res_inst_tac [("p","b`x")] trE 1),
(asm_simp_tac HOLCF_ss 1),
- (rtac (while_unfold RS ssubst) 1),
+ (stac while_unfold 1),
(res_inst_tac [("s","UU"),("t","b`UU")]ssubst 1),
(etac (flat_tr RS flat_codom RS disjE) 1),
(atac 1),
@@ -63,7 +63,7 @@
(simp_tac HOLCF_ss 1),
(asm_simp_tac HOLCF_ss 1),
(asm_simp_tac HOLCF_ss 1),
- (rtac (while_unfold RS ssubst) 1),
+ (stac while_unfold 1),
(asm_simp_tac HOLCF_ss 1)
]);
@@ -144,10 +144,10 @@
(nat_ind_tac "k" 1),
(Simp_tac 1),
(strip_tac 1),
- (rtac (while_unfold RS ssubst) 1),
+ (stac while_unfold 1),
(asm_simp_tac HOLCF_ss 1),
(rtac allI 1),
- (rtac (iterate_Suc2 RS ssubst) 1),
+ (stac iterate_Suc2 1),
(strip_tac 1),
(rtac trans 1),
(rtac while_unfold3 1),
@@ -160,7 +160,7 @@
(fn prems =>
[
(cut_facts_tac prems 1),
- (rtac (while_def2 RS ssubst) 1),
+ (stac while_def2 1),
(rtac fix_ind 1),
(rtac (allI RS adm_all) 1),
(rtac adm_eq 1),
@@ -224,7 +224,7 @@
(res_inst_tac [("P","%k. b`(iterate k (step`b`g) x)=FF")] exE 1),
(rtac loop_lemma7 1),
(resolve_tac prems 1),
- (rtac ((loop_lemma4 RS spec RS mp) RS ssubst) 1),
+ (stac (loop_lemma4 RS spec RS mp) 1),
(atac 1),
(rtac (nth_elem (1,prems) RS spec RS mp) 1),
(rtac conjI 1),