# 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