--- a/src/HOLCF/Ssum.ML Tue Jul 26 18:28:11 2005 +0200
+++ b/src/HOLCF/Ssum.ML Tue Jul 26 18:29:59 2005 +0200
@@ -1,35 +1,49 @@
(* legacy ML bindings *)
-val Iwhen_def = thm "Iwhen_def";
-val Iwhen1 = thm "Iwhen1";
-val Iwhen2 = thm "Iwhen2";
-val Iwhen3 = thm "Iwhen3";
-val less_ssum_def = thm "less_Ssum_def";
-val sinl_def = thm "sinl_def";
-val sinr_def = thm "sinr_def";
-val sscase_def = thm "sscase_def";
+val beta_sscase = thm "beta_sscase";
val cont_Iwhen1 = thm "cont_Iwhen1";
val cont_Iwhen2 = thm "cont_Iwhen2";
val cont_Iwhen3 = thm "cont_Iwhen3";
-val sinl_strict = thm "sinl_strict";
-val sinr_strict = thm "sinr_strict";
+val Exh_Ssum = thm "Exh_Ssum";
+val Iwhen1 = thm "Iwhen1";
+val Iwhen2 = thm "Iwhen2";
+val Iwhen3 = thm "Iwhen3";
+val Iwhen4 = thm "Iwhen4";
+val Iwhen5 = thm "Iwhen5";
+val Iwhen_def = thm "Iwhen_def";
+val less_sinlD = thm "less_sinlD";
+val less_sinrD = thm "less_sinrD";
+val less_ssum_def = thm "less_Ssum_def";
+val Rep_Ssum_sinl = thm "Rep_Ssum_sinl";
+val Rep_Ssum_sinr = thm "Rep_Ssum_sinr";
+val sinl_Abs_Ssum = thm "sinl_Abs_Ssum";
+val sinl_defined_iff = thm "sinl_defined_iff";
+val sinl_defined = thm "sinl_defined";
+val sinl_def = thm "sinl_def";
+val sinl_eq_sinr = thm "sinl_eq_sinr";
+val sinl_eq = thm "sinl_eq";
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 sinl_less_sinr = thm "sinl_less_sinr";
+val sinl_less = thm "sinl_less";
+val sinl_strict = thm "sinl_strict";
+val sinr_Abs_Ssum = thm "sinr_Abs_Ssum";
+val sinr_defined_iff = thm "sinr_defined_iff";
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_def = thm "sinr_def";
+val sinr_eq_sinl = thm "sinr_eq_sinl";
+val sinr_eq = thm "sinr_eq";
+val sinr_inject = thm "sinr_inject";
+val sinr_less_sinl = thm "sinr_less_sinl";
val sinr_less = thm "sinr_less";
-val sinl_less_sinr = thm "sinl_less_sinr";
-val sinr_less_sinl = thm "sinr_less_sinl";
+val sinr_strict = thm "sinr_strict";
val sscase1 = thm "sscase1";
val sscase2 = thm "sscase2";
val sscase3 = thm "sscase3";
val sscase4 = thm "sscase4";
+val sscase_def = thm "sscase_def";
+val ssum_chain_lemma = thm "ssum_chain_lemma";
+val ssumE2 = thm "ssumE2";
+val ssumE = thm "ssumE";
val Ssum_rews = [sinl_strict, sinr_strict, sinl_defined, sinr_defined,
sscase1, sscase2, sscase3];