src/HOLCF/Cprod.ML
changeset 16210 5d1b752cacc1
parent 16081 81a4b4a245b0
child 16922 2128ac2aa5db
--- a/src/HOLCF/Cprod.ML	Fri Jun 03 23:23:55 2005 +0200
+++ b/src/HOLCF/Cprod.ML	Fri Jun 03 23:26:32 2005 +0200
@@ -34,8 +34,8 @@
 val defined_cpair_rev = thm "defined_cpair_rev";
 val Exh_Cprod2 = thm "Exh_Cprod2";
 val cprodE = thm "cprodE";
-val cfst2 = thm "cfst2";
-val csnd2 = thm "csnd2";
+val cfst_cpair = thm "cfst_cpair";
+val csnd_cpair = thm "csnd_cpair";
 val cfst_strict = thm "cfst_strict";
 val csnd_strict = thm "csnd_strict";
 val surjective_pairing_Cprod2 = thm "surjective_pairing_Cprod2";
@@ -43,4 +43,4 @@
 val thelub_cprod2 = thm "thelub_cprod2";
 val csplit2 = thm "csplit2";
 val csplit3 = thm "csplit3";
-val Cprod_rews = [cfst2, csnd2, csplit2]
+val Cprod_rews = [cfst_cpair, csnd_cpair, csplit2];