--- a/src/HOLCF/Sprod.ML Fri Jun 03 23:28:21 2005 +0200
+++ b/src/HOLCF/Sprod.ML Fri Jun 03 23:29:48 2005 +0200
@@ -6,21 +6,21 @@
val sfst_def = thm "sfst_def";
val ssnd_def = thm "ssnd_def";
val ssplit_def = thm "ssplit_def";
-val inject_spair = thm "inject_spair";
+val spair_inject = thm "spair_inject";
val inst_sprod_pcpo2 = thm "inst_sprod_pcpo2";
-val strict_spair = thm "strict_spair";
-val strict_spair1 = thm "strict_spair1";
-val strict_spair2 = thm "strict_spair2";
-val strict_spair_rev = thm "strict_spair_rev";
-val defined_spair_rev = thm "defined_spair_rev";
-val defined_spair = thm "defined_spair";
+val spair_strict = thm "spair_strict";
+val spair_strict1 = thm "spair_strict1";
+val spair_strict2 = thm "spair_strict2";
+val spair_strict_rev = thm "spair_strict_rev";
+val spair_defined_rev = thm "spair_defined_rev";
+val spair_defined = thm "spair_defined";
val Exh_Sprod2 = thm "Exh_Sprod2";
val sprodE = thm "sprodE";
-val strict_sfst = thm "strict_sfst";
-val strict_ssnd = thm "strict_ssnd";
-val sfst2 = thm "sfst2";
-val ssnd2 = thm "ssnd2";
-val defined_sfstssnd = thm "defined_sfstssnd";
+val sfst_strict = thm "sfst_strict";
+val ssnd_strict = thm "ssnd_strict";
+val sfst_spair = thm "sfst_spair";
+val ssnd_spair = thm "ssnd_spair";
+val sfstssnd_defined = thm "sfstssnd_defined";
val surjective_pairing_Sprod2 = thm "surjective_pairing_Sprod2";
val ssplit1 = thm "ssplit1";
val ssplit2 = thm "ssplit2";