src/HOLCF/Pcpo.ML
changeset 16922 2128ac2aa5db
parent 15563 9e125b675253
equal deleted inserted replaced
16921:16094ed8ac6b 16922:2128ac2aa5db
     1 
     1 
     2 (* legacy ML bindings *)
     2 (* legacy ML bindings *)
     3 
     3 
       
     4 val ax_flat = thm "ax_flat";
       
     5 val ch2ch_lub = thm "ch2ch_lub";
       
     6 val chain_mono2 = thm "chain_mono2";
       
     7 val chain_UU_I_inverse2 = thm "chain_UU_I_inverse2";
       
     8 val chain_UU_I_inverse = thm "chain_UU_I_inverse";
       
     9 val chain_UU_I = thm "chain_UU_I";
       
    10 val chfin2finch = thm "chfin2finch";
       
    11 val chfin_imp_cpo = thm "chfin_imp_cpo";
       
    12 val chfin = thm "chfin";
     4 val cpo = thm "cpo";
    13 val cpo = thm "cpo";
       
    14 val diag_lub = thm "diag_lub";
       
    15 val eq_UU_iff = thm "eq_UU_iff";
       
    16 val ex_lub = thm "ex_lub";
       
    17 val flat_eq = thm "flat_eq";
       
    18 val flat_imp_chfin = thm "flat_imp_chfin";
       
    19 val increasing_chain_adm_lemma = thm "increasing_chain_adm_lemma";
       
    20 val infinite_chain_adm_lemma = thm "infinite_chain_adm_lemma";
       
    21 val is_lub_thelub = thm "is_lub_thelub";
       
    22 val is_ub_thelub = thm "is_ub_thelub";
     5 val least = thm "least";
    23 val least = thm "least";
     6 val UU_def = thm "UU_def";
    24 val lub_equal2 = thm "lub_equal2";
     7 val chfin = thm "chfin";
    25 val lub_equal = thm "lub_equal";
     8 val ax_flat = thm "ax_flat";
    26 val lub_mono2 = thm "lub_mono2";
     9 val UU_least = thm "UU_least";
    27 val lub_mono3 = thm "lub_mono3";
    10 val minimal = thm "minimal";
    28 val lub_mono = thm "lub_mono";
    11 val thelubE = thm "thelubE";
       
    12 val is_ub_thelub = thm "is_ub_thelub";
       
    13 val is_lub_thelub = thm "is_lub_thelub";
       
    14 val lub_range_shift = thm "lub_range_shift";
    29 val lub_range_shift = thm "lub_range_shift";
    15 val maxinch_is_thelub = thm "maxinch_is_thelub";
    30 val maxinch_is_thelub = thm "maxinch_is_thelub";
    16 val lub_mono = thm "lub_mono";
    31 val minimal = thm "minimal";
    17 val lub_equal = thm "lub_equal";
    32 val not_less2not_eq = thm "not_less2not_eq";
    18 val lub_mono2 = thm "lub_mono2";
    33 val notUU_I = thm "notUU_I";
    19 val lub_equal2 = thm "lub_equal2";
    34 val thelubE = thm "thelubE";
    20 val lub_mono3 = thm "lub_mono3";
    35 val UU_def = thm "UU_def";
    21 val eq_UU_iff = thm "eq_UU_iff";
       
    22 val UU_I = thm "UU_I";
    36 val UU_I = thm "UU_I";
    23 val not_less2not_eq = thm "not_less2not_eq";
    37 val UU_least = thm "UU_least";
    24 val chain_UU_I = thm "chain_UU_I";
    38 val UU_reorient = thm "UU_reorient";
    25 val chain_UU_I_inverse = thm "chain_UU_I_inverse";
       
    26 val chain_UU_I_inverse2 = thm "chain_UU_I_inverse2";
       
    27 val notUU_I = thm "notUU_I";
       
    28 val chain_mono2 = thm "chain_mono2";
       
    29 val flat_imp_chfin = thm "flat_imp_chfin";
       
    30 val flat_eq = thm "flat_eq";
       
    31 val chfin2finch = thm "chfin2finch";
       
    32 val infinite_chain_adm_lemma = thm "infinite_chain_adm_lemma";
       
    33 val increasing_chain_adm_lemma = thm "increasing_chain_adm_lemma";
       
    34 
    39 
    35 structure Pcpo =
    40 structure Pcpo =
    36 struct
    41 struct
    37   val thy = the_context ();
    42   val thy = the_context ();
    38   val UU_def = UU_def;
    43   val UU_def = UU_def;