Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
replaced pair_ss by prod_ss
authorregensbu
Wed, 15 Feb 1995 20:02:47 +0100
changeset 899 516f9e349a16
parent 898 4f9c8503d1c5
child 900 8e22076cd3ca
replaced pair_ss by prod_ss
src/HOLCF/Cprod1.ML file | annotate | diff | comparison | revisions
src/HOLCF/Cprod2.ML file | annotate | diff | comparison | revisions
src/HOLCF/Cprod3.ML file | annotate | diff | comparison | revisions 
--- 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),
--- 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)
 	]);
 
--- 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
isabelle