--- a/src/HOLCF/Ssum.ML Wed Jun 08 00:07:46 2005 +0200
+++ b/src/HOLCF/Ssum.ML Wed Jun 08 00:16:28 2005 +0200
@@ -17,18 +17,20 @@
val noteq_sinlsinr = thm "noteq_sinlsinr";
val sinl_inject = thm "sinl_inject";
val sinr_inject = thm "sinr_inject";
+val sinl_eq = thm "sinl_eq";
+val sinr_eq = thm "sinr_eq";
val sinl_defined = thm "sinl_defined";
val sinr_defined = thm "sinr_defined";
val Exh_Ssum1 = thm "Exh_Ssum1";
val ssumE = thm "ssumE";
val ssumE2 = thm "ssumE2";
+val sinl_less = thm "sinl_less";
+val sinr_less = thm "sinr_less";
+val sinl_less_sinr = thm "sinl_less_sinr";
+val sinr_less_sinl = thm "sinr_less_sinl";
val sscase1 = thm "sscase1";
val sscase2 = thm "sscase2";
val sscase3 = thm "sscase3";
-val less_ssum4a = thm "less_ssum4a";
-val less_ssum4b = thm "less_ssum4b";
-val less_ssum4c = thm "less_ssum4c";
-val less_ssum4d = thm "less_ssum4d";
val sscase4 = thm "sscase4";
val Ssum_rews = [sinl_strict, sinr_strict, sinl_defined, sinr_defined,
sscase1, sscase2, sscase3];