3 |
3 |
4 val less_cprod_def = thm "less_cprod_def"; |
4 val less_cprod_def = thm "less_cprod_def"; |
5 val refl_less_cprod = thm "refl_less_cprod"; |
5 val refl_less_cprod = thm "refl_less_cprod"; |
6 val antisym_less_cprod = thm "antisym_less_cprod"; |
6 val antisym_less_cprod = thm "antisym_less_cprod"; |
7 val trans_less_cprod = thm "trans_less_cprod"; |
7 val trans_less_cprod = thm "trans_less_cprod"; |
8 val inst_cprod_po = thm "inst_cprod_po"; |
|
9 val less_cprod4c = thm "less_cprod4c"; |
|
10 val minimal_cprod = thm "minimal_cprod"; |
8 val minimal_cprod = thm "minimal_cprod"; |
11 val UU_cprod_def = thm "UU_cprod_def"; |
|
12 val least_cprod = thm "least_cprod"; |
9 val least_cprod = thm "least_cprod"; |
13 val monofun_pair1 = thm "monofun_pair1"; |
10 val monofun_pair1 = thm "monofun_pair1"; |
14 val monofun_pair2 = thm "monofun_pair2"; |
11 val monofun_pair2 = thm "monofun_pair2"; |
15 val monofun_pair = thm "monofun_pair"; |
12 val monofun_pair = thm "monofun_pair"; |
16 val monofun_fst = thm "monofun_fst"; |
13 val monofun_fst = thm "monofun_fst"; |
30 val cont_pair2 = thm "cont_pair2"; |
27 val cont_pair2 = thm "cont_pair2"; |
31 val contlub_fst = thm "contlub_fst"; |
28 val contlub_fst = thm "contlub_fst"; |
32 val contlub_snd = thm "contlub_snd"; |
29 val contlub_snd = thm "contlub_snd"; |
33 val cont_fst = thm "cont_fst"; |
30 val cont_fst = thm "cont_fst"; |
34 val cont_snd = thm "cont_snd"; |
31 val cont_snd = thm "cont_snd"; |
35 val beta_cfun_cprod = thm "beta_cfun_cprod"; |
|
36 val inject_cpair = thm "inject_cpair"; |
32 val inject_cpair = thm "inject_cpair"; |
37 val inst_cprod_pcpo2 = thm "inst_cprod_pcpo2"; |
33 val inst_cprod_pcpo2 = thm "inst_cprod_pcpo2"; |
38 val defined_cpair_rev = thm "defined_cpair_rev"; |
34 val defined_cpair_rev = thm "defined_cpair_rev"; |
39 val Exh_Cprod2 = thm "Exh_Cprod2"; |
35 val Exh_Cprod2 = thm "Exh_Cprod2"; |
40 val cprodE = thm "cprodE"; |
36 val cprodE = thm "cprodE"; |
41 val cfst2 = thm "cfst2"; |
37 val cfst2 = thm "cfst2"; |
42 val csnd2 = thm "csnd2"; |
38 val csnd2 = thm "csnd2"; |
43 val cfst_strict = thm "cfst_strict"; |
39 val cfst_strict = thm "cfst_strict"; |
44 val csnd_strict = thm "csnd_strict"; |
40 val csnd_strict = thm "csnd_strict"; |
45 val surjective_pairing_Cprod2 = thm "surjective_pairing_Cprod2"; |
41 val surjective_pairing_Cprod2 = thm "surjective_pairing_Cprod2"; |
46 val less_cprod5c = thm "less_cprod5c"; |
|
47 val lub_cprod2 = thm "lub_cprod2"; |
42 val lub_cprod2 = thm "lub_cprod2"; |
48 val thelub_cprod2 = thm "thelub_cprod2"; |
43 val thelub_cprod2 = thm "thelub_cprod2"; |
49 val csplit2 = thm "csplit2"; |
44 val csplit2 = thm "csplit2"; |
50 val csplit3 = thm "csplit3"; |
45 val csplit3 = thm "csplit3"; |
51 val Cprod_rews = [cfst2, csnd2, csplit2] |
46 val Cprod_rews = [cfst2, csnd2, csplit2] |