src/HOLCF/Cprod.ML
changeset 16210 5d1b752cacc1
parent 16081 81a4b4a245b0
child 16922 2128ac2aa5db
equal deleted inserted replaced
16209:36ee7f6af79f 16210:5d1b752cacc1
    32 val inject_cpair = thm "inject_cpair";
    32 val inject_cpair = thm "inject_cpair";
    33 val inst_cprod_pcpo2 = thm "inst_cprod_pcpo2";
    33 val inst_cprod_pcpo2 = thm "inst_cprod_pcpo2";
    34 val defined_cpair_rev = thm "defined_cpair_rev";
    34 val defined_cpair_rev = thm "defined_cpair_rev";
    35 val Exh_Cprod2 = thm "Exh_Cprod2";
    35 val Exh_Cprod2 = thm "Exh_Cprod2";
    36 val cprodE = thm "cprodE";
    36 val cprodE = thm "cprodE";
    37 val cfst2 = thm "cfst2";
    37 val cfst_cpair = thm "cfst_cpair";
    38 val csnd2 = thm "csnd2";
    38 val csnd_cpair = thm "csnd_cpair";
    39 val cfst_strict = thm "cfst_strict";
    39 val cfst_strict = thm "cfst_strict";
    40 val csnd_strict = thm "csnd_strict";
    40 val csnd_strict = thm "csnd_strict";
    41 val surjective_pairing_Cprod2 = thm "surjective_pairing_Cprod2";
    41 val surjective_pairing_Cprod2 = thm "surjective_pairing_Cprod2";
    42 val lub_cprod2 = thm "lub_cprod2";
    42 val lub_cprod2 = thm "lub_cprod2";
    43 val thelub_cprod2 = thm "thelub_cprod2";
    43 val thelub_cprod2 = thm "thelub_cprod2";
    44 val csplit2 = thm "csplit2";
    44 val csplit2 = thm "csplit2";
    45 val csplit3 = thm "csplit3";
    45 val csplit3 = thm "csplit3";
    46 val Cprod_rews = [cfst2, csnd2, csplit2]
    46 val Cprod_rews = [cfst_cpair, csnd_cpair, csplit2];