src/HOLCF/Cprod.ML
changeset 16922 2128ac2aa5db
parent 16210 5d1b752cacc1
child 17838 3032e90c4975
equal deleted inserted replaced
16921:16094ed8ac6b 16922:2128ac2aa5db
     1 
     1 
     2 (* legacy ML bindings *)
     2 (* legacy ML bindings *)
     3 
     3 
       
     4 val antisym_less_cprod = thm "antisym_less_cprod";
       
     5 val cfst_cpair = thm "cfst_cpair";
       
     6 val cfst_def = thm "cfst_def";
       
     7 val cfst_strict = thm "cfst_strict";
       
     8 val CLet_def = thm "CLet_def";
       
     9 val cont_fst = thm "cont_fst";
       
    10 val contlub_fst = thm "contlub_fst";
       
    11 val contlub_pair1 = thm "contlub_pair1";
       
    12 val contlub_pair2 = thm "contlub_pair2";
       
    13 val contlub_snd = thm "contlub_snd";
       
    14 val cont_pair1 = thm "cont_pair1";
       
    15 val cont_pair2 = thm "cont_pair2";
       
    16 val cont_snd = thm "cont_snd";
       
    17 val cpair_def = thm "cpair_def";
       
    18 val cpair_defined_iff = thm "cpair_defined_iff";
       
    19 val cpair_eq_pair = thm "cpair_eq_pair";
       
    20 val cpair_eq = thm "cpair_eq";
       
    21 val cpair_less = thm "cpair_less";
       
    22 val cpo_cprod = thm "cpo_cprod";
       
    23 val cprodE = thm "cprodE";
       
    24 val Cprod_rews = thms "Cprod_rews";
       
    25 val csnd_cpair = thm "csnd_cpair";
       
    26 val csnd_def = thm "csnd_def";
       
    27 val csnd_strict = thm "csnd_strict";
       
    28 val csplit2 = thm "csplit2";
       
    29 val csplit3 = thm "csplit3";
       
    30 val csplit_def = thm "csplit_def";
       
    31 val defined_cpair_rev = thm "defined_cpair_rev";
       
    32 val eq_cprod = thm "eq_cprod";
       
    33 val Exh_Cprod2 = thm "Exh_Cprod2"; (* rename *)
       
    34 val inject_cpair = thm "inject_cpair";
       
    35 val inst_cprod_pcpo2 = thm "inst_cprod_pcpo2"; (**)
       
    36 val inst_cprod_pcpo = thm "inst_cprod_pcpo";
       
    37 val least_cprod = thm "least_cprod";
     4 val less_cprod_def = thm "less_cprod_def";
    38 val less_cprod_def = thm "less_cprod_def";
     5 val refl_less_cprod = thm "refl_less_cprod";
    39 val less_cprod = thm "less_cprod";
     6 val antisym_less_cprod = thm "antisym_less_cprod";
    40 val lub_cprod2 = thm "lub_cprod2"; (* *)
     7 val trans_less_cprod = thm "trans_less_cprod";
    41 val lub_cprod = thm "lub_cprod";
     8 val minimal_cprod = thm "minimal_cprod";
    42 val minimal_cprod = thm "minimal_cprod";
     9 val least_cprod = thm "least_cprod";
    43 val monofun_fst = thm "monofun_fst";
    10 val monofun_pair1 = thm "monofun_pair1";
    44 val monofun_pair1 = thm "monofun_pair1";
    11 val monofun_pair2 = thm "monofun_pair2";
    45 val monofun_pair2 = thm "monofun_pair2";
    12 val monofun_pair = thm "monofun_pair";
    46 val monofun_pair = thm "monofun_pair";
    13 val monofun_fst = thm "monofun_fst";
       
    14 val monofun_snd = thm "monofun_snd";
    47 val monofun_snd = thm "monofun_snd";
    15 val lub_cprod = thm "lub_cprod";
    48 val refl_less_cprod = thm "refl_less_cprod";
       
    49 val surjective_pairing_Cprod2 = thm "surjective_pairing_Cprod2"; (* rename *)
       
    50 val thelub_cprod2 = thm "thelub_cprod2"; (* *)
    16 val thelub_cprod = thm "thelub_cprod";
    51 val thelub_cprod = thm "thelub_cprod";
    17 val cpo_cprod = thm "cpo_cprod";
    52 val trans_less_cprod = thm "trans_less_cprod";
    18 val cpair_def = thm "cpair_def";
       
    19 val cfst_def = thm "cfst_def";
       
    20 val csnd_def = thm "csnd_def";
       
    21 val csplit_def = thm "csplit_def";
       
    22 val CLet_def = thm "CLet_def";
       
    23 val inst_cprod_pcpo = thm "inst_cprod_pcpo";
       
    24 val contlub_pair1 = thm "contlub_pair1";
       
    25 val contlub_pair2 = thm "contlub_pair2";
       
    26 val cont_pair1 = thm "cont_pair1";
       
    27 val cont_pair2 = thm "cont_pair2";
       
    28 val contlub_fst = thm "contlub_fst";
       
    29 val contlub_snd = thm "contlub_snd";
       
    30 val cont_fst = thm "cont_fst";
       
    31 val cont_snd = thm "cont_snd";
       
    32 val inject_cpair = thm "inject_cpair";
       
    33 val inst_cprod_pcpo2 = thm "inst_cprod_pcpo2";
       
    34 val defined_cpair_rev = thm "defined_cpair_rev";
       
    35 val Exh_Cprod2 = thm "Exh_Cprod2";
       
    36 val cprodE = thm "cprodE";
       
    37 val cfst_cpair = thm "cfst_cpair";
       
    38 val csnd_cpair = thm "csnd_cpair";
       
    39 val cfst_strict = thm "cfst_strict";
       
    40 val csnd_strict = thm "csnd_strict";
       
    41 val surjective_pairing_Cprod2 = thm "surjective_pairing_Cprod2";
       
    42 val lub_cprod2 = thm "lub_cprod2";
       
    43 val thelub_cprod2 = thm "thelub_cprod2";
       
    44 val csplit2 = thm "csplit2";
       
    45 val csplit3 = thm "csplit3";
       
    46 val Cprod_rews = [cfst_cpair, csnd_cpair, csplit2];