--- a/src/HOLCF/Cprod3.ML Wed Feb 08 11:30:00 1995 +0100
+++ b/src/HOLCF/Cprod3.ML Wed Feb 15 20:02:47 1995 +0100
@@ -27,9 +27,9 @@
(rtac (monofun_pair1 RS ch2ch_monofun) 1),
(atac 1),
(rtac allI 1),
- (simp_tac pair_ss 1),
+ (simp_tac prod_ss 1),
(rtac sym 1),
- (simp_tac pair_ss 1),
+ (simp_tac prod_ss 1),
(rtac (lub_const RS thelubI) 1)
]);
@@ -58,7 +58,7 @@
(cut_facts_tac prems 1),
(res_inst_tac [("f1","Pair")] (arg_cong RS cong) 1),
(rtac sym 1),
- (simp_tac pair_ss 1),
+ (simp_tac prod_ss 1),
(rtac (lub_const RS thelubI) 1),
(rtac lub_equal 1),
(atac 1),
@@ -66,7 +66,7 @@
(rtac (monofun_pair2 RS ch2ch_monofun) 1),
(atac 1),
(rtac allI 1),
- (simp_tac pair_ss 1)
+ (simp_tac prod_ss 1)
]);
qed_goal "contlub_pair2" Cprod3.thy "contlub(Pair(x))"
@@ -103,7 +103,7 @@
(strip_tac 1),
(rtac (lub_cprod RS thelubI RS ssubst) 1),
(atac 1),
- (simp_tac pair_ss 1)
+ (simp_tac prod_ss 1)
]);
qed_goal "contlub_snd" Cprod3.thy "contlub(snd)"
@@ -113,7 +113,7 @@
(strip_tac 1),
(rtac (lub_cprod RS thelubI RS ssubst) 1),
(atac 1),
- (simp_tac pair_ss 1)
+ (simp_tac prod_ss 1)
]);
qed_goal "contX_fst" Cprod3.thy "contX(fst)"
@@ -214,7 +214,7 @@
(rtac (beta_cfun_cprod RS ssubst) 1),
(rtac (beta_cfun RS ssubst) 1),
(rtac contX_fst 1),
- (simp_tac pair_ss 1)
+ (simp_tac prod_ss 1)
]);
qed_goalw "csnd2" Cprod3.thy [csnd_def,cpair_def]
@@ -225,7 +225,7 @@
(rtac (beta_cfun_cprod RS ssubst) 1),
(rtac (beta_cfun RS ssubst) 1),
(rtac contX_snd 1),
- (simp_tac pair_ss 1)
+ (simp_tac prod_ss 1)
]);
qed_goalw "surjective_pairing_Cprod2" Cprod3.thy