--- a/src/HOLCF/Sprod.ML Wed Jun 08 00:16:28 2005 +0200
+++ b/src/HOLCF/Sprod.ML Wed Jun 08 00:18:26 2005 +0200
@@ -6,7 +6,6 @@
val sfst_def = thm "sfst_def";
val ssnd_def = thm "ssnd_def";
val ssplit_def = thm "ssplit_def";
-val spair_inject = thm "spair_inject";
val inst_sprod_pcpo2 = thm "inst_sprod_pcpo2";
val spair_strict = thm "spair_strict";
val spair_strict1 = thm "spair_strict1";
@@ -14,6 +13,8 @@
val spair_strict_rev = thm "spair_strict_rev";
val spair_defined_rev = thm "spair_defined_rev";
val spair_defined = thm "spair_defined";
+val spair_eq = thm "spair_eq";
+val spair_inject = thm "spair_inject";
val Exh_Sprod2 = thm "Exh_Sprod2";
val sprodE = thm "sprodE";
val sfst_strict = thm "sfst_strict";
@@ -22,6 +23,8 @@
val ssnd_spair = thm "ssnd_spair";
val sfstssnd_defined = thm "sfstssnd_defined";
val surjective_pairing_Sprod2 = thm "surjective_pairing_Sprod2";
+val less_sprod = thm "less_sprod";
+val spair_less = thm "spair_less";
val ssplit1 = thm "ssplit1";
val ssplit2 = thm "ssplit2";
val ssplit3 = thm "ssplit3";