--- a/src/HOLCF/Sprod3.ML Tue Oct 17 08:41:42 2000 +0200
+++ b/src/HOLCF/Sprod3.ML Tue Oct 17 10:20:43 2000 +0200
@@ -195,7 +195,7 @@
by (rtac chain_UU_I_inverse 1);
by (rtac allI 1);
by (rtac strict_Isfst 1);
-by (rtac swap 1);
+by (rtac contrapos_np 1);
by (etac (defined_IsfstIssnd RS conjunct2) 2);
by (fast_tac (HOL_cs addSDs [monofun_Issnd RS ch2ch_monofun RS chain_UU_I RS spec]) 1);
qed "contlub_Isfst";
@@ -214,7 +214,7 @@
by (rtac chain_UU_I_inverse 1);
by (rtac allI 1);
by (rtac strict_Issnd 1);
-by (rtac swap 1);
+by (rtac contrapos_np 1);
by (etac (defined_IsfstIssnd RS conjunct1) 2);
by (fast_tac (HOL_cs addSDs [monofun_Isfst RS ch2ch_monofun RS chain_UU_I RS spec]) 1);
qed "contlub_Issnd";