--- a/src/HOLCF/Cfun2.ML Thu Sep 26 12:50:48 1996 +0200
+++ b/src/HOLCF/Cfun2.ML Thu Sep 26 15:14:23 1996 +0200
@@ -15,7 +15,7 @@
qed_goal "less_cfun" Cfun2.thy "( f1 << f2 ) = (fapp(f1) << fapp(f2))"
(fn prems =>
[
- (rtac (inst_cfun_po RS ssubst) 1),
+ (stac inst_cfun_po 1),
(fold_goals_tac [less_cfun_def]),
(rtac refl 1)
]);
@@ -27,8 +27,8 @@
qed_goalw "minimal_cfun" Cfun2.thy [UU_cfun_def] "UU_cfun << f"
(fn prems =>
[
- (rtac (less_cfun RS ssubst) 1),
- (rtac (Abs_Cfun_inverse2 RS ssubst) 1),
+ (stac less_cfun 1),
+ (stac Abs_Cfun_inverse2 1),
(rtac cont_const 1),
(fold_goals_tac [UU_fun_def]),
(rtac minimal_fun 1)
@@ -112,10 +112,10 @@
qed_goal "strictI" Cfun2.thy "f`x = UU ==> f`UU = UU" (fn prems => [
- cut_facts_tac prems 1,
- rtac (eq_UU_iff RS iffD2) 1,
- etac subst 1,
- rtac (minimal RS monofun_cfun_arg) 1]);
+ cut_facts_tac prems 1,
+ rtac (eq_UU_iff RS iffD2) 1,
+ etac subst 1,
+ rtac (minimal RS monofun_cfun_arg) 1]);
(* ------------------------------------------------------------------------ *)
@@ -184,7 +184,7 @@
(etac lub_cfun_mono 1),
(rtac contlubI 1),
(strip_tac 1),
- (rtac (contlub_cfun_arg RS ext RS ssubst) 1),
+ (stac (contlub_cfun_arg RS ext) 1),
(atac 1),
(etac ex_lubcfun 1),
(atac 1)
@@ -203,14 +203,14 @@
(rtac conjI 1),
(rtac ub_rangeI 1),
(rtac allI 1),
- (rtac (less_cfun RS ssubst) 1),
- (rtac (Abs_Cfun_inverse2 RS ssubst) 1),
+ (stac less_cfun 1),
+ (stac Abs_Cfun_inverse2 1),
(etac cont_lubcfun 1),
(rtac (lub_fun RS is_lubE RS conjunct1 RS ub_rangeE RS spec) 1),
(etac (monofun_fapp1 RS ch2ch_monofun) 1),
(strip_tac 1),
- (rtac (less_cfun RS ssubst) 1),
- (rtac (Abs_Cfun_inverse2 RS ssubst) 1),
+ (stac less_cfun 1),
+ (stac Abs_Cfun_inverse2 1),
(etac cont_lubcfun 1),
(rtac (lub_fun RS is_lubE RS conjunct2 RS spec RS mp) 1),
(etac (monofun_fapp1 RS ch2ch_monofun) 1),
@@ -255,9 +255,9 @@
(fn prems =>
[
(rtac (less_cfun RS iffD2) 1),
- (rtac (Abs_Cfun_inverse2 RS ssubst) 1),
+ (stac Abs_Cfun_inverse2 1),
(resolve_tac prems 1),
- (rtac (Abs_Cfun_inverse2 RS ssubst) 1),
+ (stac Abs_Cfun_inverse2 1),
(resolve_tac prems 1),
(resolve_tac prems 1)
]);