equal
deleted
inserted
replaced
1 |
|
2 (* legacy ML bindings *) |
|
3 |
|
4 val inst_ssum_po = thm "inst_ssum_po"; |
|
5 val less_ssum3a = thm "less_ssum3a"; |
|
6 val less_ssum3b = thm "less_ssum3b"; |
|
7 val less_ssum3c = thm "less_ssum3c"; |
|
8 val less_ssum3d = thm "less_ssum3d"; |
|
9 val minimal_ssum = thm "minimal_ssum"; |
|
10 val UU_ssum_def = thm "UU_ssum_def"; |
|
11 val least_ssum = thm "least_ssum"; |
|
12 val monofun_Isinl = thm "monofun_Isinl"; |
|
13 val monofun_Isinr = thm "monofun_Isinr"; |
|
14 val monofun_Iwhen1 = thm "monofun_Iwhen1"; |
|
15 val monofun_Iwhen2 = thm "monofun_Iwhen2"; |
|
16 val monofun_Iwhen3 = thm "monofun_Iwhen3"; |
|
17 val ssum_lemma1 = thm "ssum_lemma1"; |
|
18 val ssum_lemma2 = thm "ssum_lemma2"; |
|
19 val ssum_lemma3 = thm "ssum_lemma3"; |
|
20 val ssum_lemma4 = thm "ssum_lemma4"; |
|
21 val ssum_lemma5 = thm "ssum_lemma5"; |
|
22 val ssum_lemma6 = thm "ssum_lemma6"; |
|
23 val ssum_lemma7 = thm "ssum_lemma7"; |
|
24 val ssum_lemma8 = thm "ssum_lemma8"; |
|
25 val lub_ssum1a = thm "lub_ssum1a"; |
|
26 val lub_ssum1b = thm "lub_ssum1b"; |
|
27 val thelub_ssum1a = thm "thelub_ssum1a"; |
|
28 val thelub_ssum1b = thm "thelub_ssum1b"; |
|
29 val cpo_ssum = thm "cpo_ssum"; |
|