--- a/src/HOLCF/Tr1.ML Thu Sep 26 12:50:48 1996 +0200
+++ b/src/HOLCF/Tr1.ML Thu Sep 26 15:14:23 1996 +0200
@@ -23,7 +23,7 @@
(rtac (rep_tr_iso RS subst) 1),
(rtac (rep_tr_iso RS subst) 1),
(rtac cfun_arg_cong 1),
- (rtac ((abs_tr_iso RS allI) RS ((rep_tr_iso RS allI) RS iso_strict ) RS conjunct2 RS ssubst) 1),
+ (stac ((abs_tr_iso RS allI) RS ((rep_tr_iso RS allI) RS iso_strict ) RS conjunct2) 1),
(etac (eq_UU_iff RS ssubst) 1)
]),
prove_goalw Tr1.thy [FF_def] "~FF << UU"
@@ -36,7 +36,7 @@
(rtac (rep_tr_iso RS subst) 1),
(rtac (rep_tr_iso RS subst) 1),
(rtac cfun_arg_cong 1),
- (rtac ((abs_tr_iso RS allI) RS ((rep_tr_iso RS allI) RS iso_strict ) RS conjunct2 RS ssubst) 1),
+ (stac ((abs_tr_iso RS allI) RS ((rep_tr_iso RS allI) RS iso_strict ) RS conjunct2) 1),
(etac (eq_UU_iff RS ssubst) 1)
]),
prove_goalw Tr1.thy [FF_def,TT_def] "~TT << FF"