--- a/src/HOLCF/Cprod2.ML Wed Oct 04 13:12:14 1995 +0100
+++ b/src/HOLCF/Cprod2.ML Wed Oct 04 14:01:44 1995 +0100
@@ -16,10 +16,7 @@
(rtac (inst_cprod_po RS ssubst) 1),
(rtac (less_cprod1b RS ssubst) 1),
(hyp_subst_tac 1),
- (asm_simp_tac prod_ss 1),
- (rtac conjI 1),
- (rtac minimal 1),
- (rtac minimal 1)
+ (Asm_simp_tac 1)
]);
qed_goal "less_cprod3b" Cprod2.thy
@@ -80,8 +77,7 @@
(rtac (less_fun RS iffD2) 1),
(strip_tac 1),
(rtac (less_cprod3b RS iffD2) 1),
- (simp_tac prod_ss 1),
- (asm_simp_tac Cfun_ss 1)
+ (Simp_tac 1)
]);
qed_goalw "monofun_pair2" Cprod2.thy [monofun] "monofun(Pair(x))"
@@ -89,8 +85,7 @@
[
(strip_tac 1),
(rtac (less_cprod3b RS iffD2) 1),
- (simp_tac prod_ss 1),
- (asm_simp_tac Cfun_ss 1)
+ (Simp_tac 1)
]);
qed_goal "monofun_pair" Cprod2.thy
@@ -118,7 +113,7 @@
(hyp_subst_tac 1),
(res_inst_tac [("p","y")] PairE 1),
(hyp_subst_tac 1),
- (asm_simp_tac prod_ss 1),
+ (Asm_simp_tac 1),
(etac (less_cprod4c RS conjunct1) 1)
]);
@@ -130,7 +125,7 @@
(hyp_subst_tac 1),
(res_inst_tac [("p","y")] PairE 1),
(hyp_subst_tac 1),
- (asm_simp_tac prod_ss 1),
+ (Asm_simp_tac 1),
(etac (less_cprod4c RS conjunct2) 1)
]);