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]; |