src/HOLCF/Pcpo.ML
changeset 16922 2128ac2aa5db
parent 15563 9e125b675253
--- a/src/HOLCF/Pcpo.ML	Tue Jul 26 18:28:11 2005 +0200
+++ b/src/HOLCF/Pcpo.ML	Tue Jul 26 18:29:59 2005 +0200
@@ -1,36 +1,41 @@
 
 (* legacy ML bindings *)
 
-val cpo = thm "cpo";
-val least = thm "least";
-val UU_def = thm "UU_def";
+val ax_flat = thm "ax_flat";
+val ch2ch_lub = thm "ch2ch_lub";
+val chain_mono2 = thm "chain_mono2";
+val chain_UU_I_inverse2 = thm "chain_UU_I_inverse2";
+val chain_UU_I_inverse = thm "chain_UU_I_inverse";
+val chain_UU_I = thm "chain_UU_I";
+val chfin2finch = thm "chfin2finch";
+val chfin_imp_cpo = thm "chfin_imp_cpo";
 val chfin = thm "chfin";
-val ax_flat = thm "ax_flat";
-val UU_least = thm "UU_least";
-val minimal = thm "minimal";
-val thelubE = thm "thelubE";
+val cpo = thm "cpo";
+val diag_lub = thm "diag_lub";
+val eq_UU_iff = thm "eq_UU_iff";
+val ex_lub = thm "ex_lub";
+val flat_eq = thm "flat_eq";
+val flat_imp_chfin = thm "flat_imp_chfin";
+val increasing_chain_adm_lemma = thm "increasing_chain_adm_lemma";
+val infinite_chain_adm_lemma = thm "infinite_chain_adm_lemma";
+val is_lub_thelub = thm "is_lub_thelub";
 val is_ub_thelub = thm "is_ub_thelub";
-val is_lub_thelub = thm "is_lub_thelub";
-val lub_range_shift = thm "lub_range_shift";
-val maxinch_is_thelub = thm "maxinch_is_thelub";
-val lub_mono = thm "lub_mono";
+val least = thm "least";
+val lub_equal2 = thm "lub_equal2";
 val lub_equal = thm "lub_equal";
 val lub_mono2 = thm "lub_mono2";
-val lub_equal2 = thm "lub_equal2";
 val lub_mono3 = thm "lub_mono3";
-val eq_UU_iff = thm "eq_UU_iff";
-val UU_I = thm "UU_I";
+val lub_mono = thm "lub_mono";
+val lub_range_shift = thm "lub_range_shift";
+val maxinch_is_thelub = thm "maxinch_is_thelub";
+val minimal = thm "minimal";
 val not_less2not_eq = thm "not_less2not_eq";
-val chain_UU_I = thm "chain_UU_I";
-val chain_UU_I_inverse = thm "chain_UU_I_inverse";
-val chain_UU_I_inverse2 = thm "chain_UU_I_inverse2";
 val notUU_I = thm "notUU_I";
-val chain_mono2 = thm "chain_mono2";
-val flat_imp_chfin = thm "flat_imp_chfin";
-val flat_eq = thm "flat_eq";
-val chfin2finch = thm "chfin2finch";
-val infinite_chain_adm_lemma = thm "infinite_chain_adm_lemma";
-val increasing_chain_adm_lemma = thm "increasing_chain_adm_lemma";
+val thelubE = thm "thelubE";
+val UU_def = thm "UU_def";
+val UU_I = thm "UU_I";
+val UU_least = thm "UU_least";
+val UU_reorient = thm "UU_reorient";
 
 structure Pcpo =
 struct