--- a/src/HOLCF/Porder.ML Tue Jul 26 18:28:11 2005 +0200
+++ b/src/HOLCF/Porder.ML Tue Jul 26 18:29:59 2005 +0200
@@ -1,44 +1,46 @@
(* legacy ML bindings *)
-val refl_less = thm "refl_less";
+val antisym_less_inverse = thm "antisym_less_inverse";
val antisym_less = thm "antisym_less";
-val trans_less = thm "trans_less";
-val minimal2UU = thm "minimal2UU";
-val antisym_less_inverse = thm "antisym_less_inverse";
+val bin_chainmax = thm "bin_chainmax";
+val bin_chain = thm "bin_chain";
val box_less = thm "box_less";
-val po_eq_conv = thm "po_eq_conv";
-val is_ub_def = thm "is_ub_def";
-val is_lub_def = thm "is_lub_def";
-val tord_def = thm "tord_def";
val chain_def = thm "chain_def";
-val max_in_chain_def = thm "max_in_chain_def";
-val finite_chain_def = thm "finite_chain_def";
-val lub_def = thm "lub_def";
-val unique_lub = thm "unique_lub";
-val chain_mono = thm "chain_mono";
-val chain_mono3 = thm "chain_mono3";
-val chain_tord = thm "chain_tord";
-val lub = thm "lub";
-val lubI = thm "lubI";
-val thelubI = thm "thelubI";
-val lub_singleton = thm "lub_singleton";
-val is_lubD1 = thm "is_lubD1";
-val is_lub_lub = thm "is_lub_lub";
-val is_lubI = thm "is_lubI";
val chainE = thm "chainE";
val chainI = thm "chainI";
+val chain_mono3 = thm "chain_mono3";
+val chain_mono = thm "chain_mono";
val chain_shift = thm "chain_shift";
-val ub_rangeD = thm "ub_rangeD";
-val ub_rangeI = thm "ub_rangeI";
+val chain_tord = thm "chain_tord";
+val finite_chain_def = thm "finite_chain_def";
+val is_lubD1 = thm "is_lubD1";
+val is_lub_def = thm "is_lub_def";
+val is_lubI = thm "is_lubI";
+val is_lub_lub = thm "is_lub_lub";
+val is_lub_range_shift = thm "is_lub_range_shift";
+val is_ub_def = thm "is_ub_def";
val is_ub_lub = thm "is_ub_lub";
-val lub_finch1 = thm "lub_finch1";
-val lub_finch2 = thm "lub_finch2";
-val bin_chain = thm "bin_chain";
-val bin_chainmax = thm "bin_chainmax";
+val is_ub_range_shift = thm "is_ub_range_shift";
val lub_bin_chain = thm "lub_bin_chain";
val lub_chain_maxelem = thm "lub_chain_maxelem";
val lub_const = thm "lub_const";
+val lub_def = thm "lub_def";
+val lub_finch1 = thm "lub_finch1";
+val lub_finch2 = thm "lub_finch2";
+val lubI = thm "lubI";
+val lub_singleton = thm "lub_singleton";
+val lub = thm "lub";
+val max_in_chain_def = thm "max_in_chain_def";
+val minimal2UU = thm "minimal2UU";
+val po_eq_conv = thm "po_eq_conv";
+val refl_less = thm "refl_less";
+val thelubI = thm "thelubI";
+val tord_def = thm "tord_def";
+val trans_less = thm "trans_less";
+val ub_rangeD = thm "ub_rangeD";
+val ub_rangeI = thm "ub_rangeI";
+val unique_lub = thm "unique_lub";
structure Porder =
struct