# HG changeset patch
# User regensbu
# Date 792874967 -3600
# Node ID 516f9e349a16b87048aadf801d26109e59a80799
# Parent  4f9c8503d1c58c3ade7be9528bebe430a3fc8888
replaced pair_ss by prod_ss

diff -r 4f9c8503d1c5 -r 516f9e349a16 src/HOLCF/Cprod1.ML
--- a/src/HOLCF/Cprod1.ML	Wed Feb 08 11:30:00 1995 +0100
+++ b/src/HOLCF/Cprod1.ML	Wed Feb 15 20:02:47 1995 +0100
@@ -69,7 +69,7 @@
 	[
 	(res_inst_tac [("p","p")] PairE 1),
 	(hyp_subst_tac 1),
-	(simp_tac pair_ss 1),
+	(simp_tac prod_ss 1),
 	(simp_tac Cfun_ss 1)
 	]);
 
@@ -105,7 +105,7 @@
 	(dtac less_cprod2c 1),
 	(dtac less_cprod2c 1),
 	(rtac (less_cprod1b RS ssubst) 1),
-	(simp_tac pair_ss 1),
+	(simp_tac prod_ss 1),
 	(etac conjE 1),
 	(etac conjE 1),
 	(rtac conjI 1),
diff -r 4f9c8503d1c5 -r 516f9e349a16 src/HOLCF/Cprod2.ML
--- a/src/HOLCF/Cprod2.ML	Wed Feb 08 11:30:00 1995 +0100
+++ b/src/HOLCF/Cprod2.ML	Wed Feb 15 20:02:47 1995 +0100
@@ -16,7 +16,7 @@
 	(rtac (inst_cprod_po RS ssubst) 1),
 	(rtac (less_cprod1b RS ssubst) 1),
 	(hyp_subst_tac 1),
-	(asm_simp_tac pair_ss  1),
+	(asm_simp_tac prod_ss  1),
 	(rtac conjI 1),
 	(rtac minimal 1),
 	(rtac minimal 1)
@@ -80,7 +80,7 @@
 	(rtac (less_fun RS iffD2) 1),
 	(strip_tac 1),
 	(rtac (less_cprod3b RS iffD2) 1),
-	(simp_tac pair_ss 1),
+	(simp_tac prod_ss 1),
 	(asm_simp_tac Cfun_ss 1)
 	]);
 
@@ -89,7 +89,7 @@
 	[
 	(strip_tac 1),
 	(rtac (less_cprod3b RS iffD2) 1),
-	(simp_tac pair_ss 1),
+	(simp_tac prod_ss 1),
 	(asm_simp_tac Cfun_ss 1)
 	]);
 
@@ -118,7 +118,7 @@
 	(hyp_subst_tac 1),
 	(res_inst_tac [("p","y")] PairE 1),
 	(hyp_subst_tac 1),
-	(asm_simp_tac pair_ss  1),
+	(asm_simp_tac prod_ss  1),
 	(etac (less_cprod4c RS conjunct1) 1)
 	]);
 
@@ -130,7 +130,7 @@
 	(hyp_subst_tac 1),
 	(res_inst_tac [("p","y")] PairE 1),
 	(hyp_subst_tac 1),
-	(asm_simp_tac pair_ss  1),
+	(asm_simp_tac prod_ss  1),
 	(etac (less_cprod4c RS conjunct2) 1)
 	]);
 
diff -r 4f9c8503d1c5 -r 516f9e349a16 src/HOLCF/Cprod3.ML
--- 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