equal
deleted
inserted
replaced
22 val cfst_def = thm "cfst_def"; |
22 val cfst_def = thm "cfst_def"; |
23 val csnd_def = thm "csnd_def"; |
23 val csnd_def = thm "csnd_def"; |
24 val csplit_def = thm "csplit_def"; |
24 val csplit_def = thm "csplit_def"; |
25 val CLet_def = thm "CLet_def"; |
25 val CLet_def = thm "CLet_def"; |
26 val inst_cprod_pcpo = thm "inst_cprod_pcpo"; |
26 val inst_cprod_pcpo = thm "inst_cprod_pcpo"; |
27 val Cprod3_lemma1 = thm "Cprod3_lemma1"; |
|
28 val contlub_pair1 = thm "contlub_pair1"; |
27 val contlub_pair1 = thm "contlub_pair1"; |
29 val Cprod3_lemma2 = thm "Cprod3_lemma2"; |
|
30 val contlub_pair2 = thm "contlub_pair2"; |
28 val contlub_pair2 = thm "contlub_pair2"; |
31 val cont_pair1 = thm "cont_pair1"; |
29 val cont_pair1 = thm "cont_pair1"; |
32 val cont_pair2 = thm "cont_pair2"; |
30 val cont_pair2 = thm "cont_pair2"; |
33 val contlub_fst = thm "contlub_fst"; |
31 val contlub_fst = thm "contlub_fst"; |
34 val contlub_snd = thm "contlub_snd"; |
32 val contlub_snd = thm "contlub_snd"; |