src/HOLCF/Ssum.ML
changeset 16060 833be7f71ecd
parent 15607 30576c645e91
child 16211 faa9691da2bc
equal deleted inserted replaced
16059:dab0d004732f 16060:833be7f71ecd
     1 
     1 
     2 (* legacy ML bindings *)
     2 (* legacy ML bindings *)
     3 
     3 
     4 val Isinl_def = thm "Isinl_def";
       
     5 val Isinr_def = thm "Isinr_def";
       
     6 val Iwhen_def = thm "Iwhen_def";
     4 val Iwhen_def = thm "Iwhen_def";
     7 val inj_on_Abs_Ssum = thm "inj_on_Abs_Ssum";
       
     8 val strict_IsinlIsinr = thm "strict_IsinlIsinr";
       
     9 val noteq_IsinlIsinr = thm "noteq_IsinlIsinr";
       
    10 val inject_Isinl = thm "inject_Isinl";
       
    11 val inject_Isinr = thm "inject_Isinr";
       
    12 val inject_Isinl_rev = thm "inject_Isinl_rev";
       
    13 val inject_Isinr_rev = thm "inject_Isinr_rev";
       
    14 val Exh_Ssum = thm "Exh_Ssum";
       
    15 val IssumE = thm "IssumE";
       
    16 val IssumE2 = thm "IssumE2";
       
    17 val Iwhen1 = thm "Iwhen1";
     5 val Iwhen1 = thm "Iwhen1";
    18 val Iwhen2 = thm "Iwhen2";
     6 val Iwhen2 = thm "Iwhen2";
    19 val Iwhen3 = thm "Iwhen3";
     7 val Iwhen3 = thm "Iwhen3";
    20 val less_ssum_def = thm "less_ssum_def";
     8 val less_ssum_def = thm "less_ssum_def";
    21 val less_ssum1a = thm "less_ssum1a";
       
    22 val less_ssum1b = thm "less_ssum1b";
       
    23 val less_ssum1c = thm "less_ssum1c";
       
    24 val less_ssum1d = thm "less_ssum1d";
       
    25 val less_ssum2a = thm "less_ssum2a";
       
    26 val less_ssum2b = thm "less_ssum2b";
       
    27 val less_ssum2c = thm "less_ssum2c";
       
    28 val less_ssum2d = thm "less_ssum2d";
       
    29 val refl_less_ssum = thm "refl_less_ssum";
       
    30 val antisym_less_ssum = thm "antisym_less_ssum";
       
    31 val trans_less_ssum = thm "trans_less_ssum";
       
    32 val inst_ssum_po = thm "inst_ssum_po";
       
    33 val less_ssum3a = thm "less_ssum3a";
       
    34 val less_ssum3b = thm "less_ssum3b";
       
    35 val less_ssum3c = thm "less_ssum3c";
       
    36 val less_ssum3d = thm "less_ssum3d";
       
    37 val minimal_ssum = thm "minimal_ssum";
       
    38 val UU_ssum_def = thm "UU_ssum_def";
       
    39 val least_ssum = thm "least_ssum";
       
    40 val monofun_Isinl = thm "monofun_Isinl";
       
    41 val monofun_Isinr = thm "monofun_Isinr";
       
    42 val monofun_Iwhen1 = thm "monofun_Iwhen1";
       
    43 val monofun_Iwhen2 = thm "monofun_Iwhen2";
       
    44 val monofun_Iwhen3 = thm "monofun_Iwhen3";
       
    45 val ssum_lemma1 = thm "ssum_lemma1";
       
    46 val ssum_lemma2 = thm "ssum_lemma2";
       
    47 val ssum_lemma3 = thm "ssum_lemma3";
       
    48 val ssum_lemma4 = thm "ssum_lemma4";
       
    49 val ssum_lemma5 = thm "ssum_lemma5";
       
    50 val ssum_lemma6 = thm "ssum_lemma6";
       
    51 val ssum_lemma7 = thm "ssum_lemma7";
       
    52 val ssum_lemma8 = thm "ssum_lemma8";
       
    53 val lub_ssum1a = thm "lub_ssum1a";
       
    54 val lub_ssum1b = thm "lub_ssum1b";
       
    55 val thelub_ssum1a = thm "thelub_ssum1a";
       
    56 val thelub_ssum1b = thm "thelub_ssum1b";
       
    57 val cpo_ssum = thm "cpo_ssum";
       
    58 val sinl_def = thm "sinl_def";
     9 val sinl_def = thm "sinl_def";
    59 val sinr_def = thm "sinr_def";
    10 val sinr_def = thm "sinr_def";
    60 val sscase_def = thm "sscase_def";
    11 val sscase_def = thm "sscase_def";
    61 val inst_ssum_pcpo = thm "inst_ssum_pcpo";
       
    62 val contlub_Isinl = thm "contlub_Isinl";
       
    63 val contlub_Isinr = thm "contlub_Isinr";
       
    64 val cont_Isinl = thm "cont_Isinl";
       
    65 val cont_Isinr = thm "cont_Isinr";
       
    66 val contlub_Iwhen1 = thm "contlub_Iwhen1";
       
    67 val contlub_Iwhen2 = thm "contlub_Iwhen2";
       
    68 val ssum_lemma9 = thm "ssum_lemma9";
       
    69 val ssum_lemma10 = thm "ssum_lemma10";
       
    70 val ssum_lemma11 = thm "ssum_lemma11";
       
    71 val ssum_lemma12 = thm "ssum_lemma12";
       
    72 val ssum_lemma13 = thm "ssum_lemma13";
       
    73 val contlub_Iwhen3 = thm "contlub_Iwhen3";
       
    74 val cont_Iwhen1 = thm "cont_Iwhen1";
    12 val cont_Iwhen1 = thm "cont_Iwhen1";
    75 val cont_Iwhen2 = thm "cont_Iwhen2";
    13 val cont_Iwhen2 = thm "cont_Iwhen2";
    76 val cont_Iwhen3 = thm "cont_Iwhen3";
    14 val cont_Iwhen3 = thm "cont_Iwhen3";
    77 val strict_sinl = thm "strict_sinl";
    15 val strict_sinl = thm "strict_sinl";
    78 val strict_sinr = thm "strict_sinr";
    16 val strict_sinr = thm "strict_sinr";
    89 val sscase3 = thm "sscase3";
    27 val sscase3 = thm "sscase3";
    90 val less_ssum4a = thm "less_ssum4a";
    28 val less_ssum4a = thm "less_ssum4a";
    91 val less_ssum4b = thm "less_ssum4b";
    29 val less_ssum4b = thm "less_ssum4b";
    92 val less_ssum4c = thm "less_ssum4c";
    30 val less_ssum4c = thm "less_ssum4c";
    93 val less_ssum4d = thm "less_ssum4d";
    31 val less_ssum4d = thm "less_ssum4d";
    94 val ssum_chainE = thm "ssum_chainE";
       
    95 val thelub_ssum2a = thm "thelub_ssum2a";
       
    96 val thelub_ssum2b = thm "thelub_ssum2b";
       
    97 val thelub_ssum2a_rev = thm "thelub_ssum2a_rev";
       
    98 val thelub_ssum2b_rev = thm "thelub_ssum2b_rev";
       
    99 val thelub_ssum3 = thm "thelub_ssum3";
       
   100 val sscase4 = thm "sscase4";
    32 val sscase4 = thm "sscase4";
   101 val Ssum_rews = [strict_sinl, strict_sinr, defined_sinl, defined_sinr,
    33 val Ssum_rews = [strict_sinl, strict_sinr, defined_sinl, defined_sinr,
   102                 sscase1, sscase2, sscase3]
    34                 sscase1, sscase2, sscase3]