author | haftmann |
Tue, 06 Dec 2005 09:04:09 +0100 | |
changeset 18358 | 0a733e11021a |
parent 17838 | 3032e90c4975 |
permissions | -rw-r--r-- |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
1 |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
2 |
(* legacy ML bindings *) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
3 |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
4 |
val antisym_less_up = thm "antisym_less_up"; |
17838 | 5 |
val compact_up = thm "compact_up"; |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
6 |
val cont_Ifup1 = thm "cont_Ifup1"; |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
7 |
val cont_Ifup2 = thm "cont_Ifup2"; |
16922 | 8 |
val cont_Iup = thm "cont_Iup"; |
9 |
val cpo_up = thm "cpo_up"; |
|
16753 | 10 |
val Exh_Up = thm "Exh_Up"; |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
11 |
val fup1 = thm "fup1"; |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
12 |
val fup2 = thm "fup2"; |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
13 |
val fup3 = thm "fup3"; |
16922 | 14 |
val fup_def = thm "fup_def"; |
15 |
val inst_up_pcpo = thm "inst_up_pcpo"; |
|
16 |
val is_lub_Iup = thm "is_lub_Iup"; |
|
17 |
val Iup_less = thm "Iup_less"; |
|
18 |
val least_up = thm "least_up"; |
|
19 |
val less_up_def = thm "less_up_def"; |
|
20 |
val minimal_up = thm "minimal_up"; |
|
21 |
val monofun_Ifup2 = thm "monofun_Ifup2"; |
|
22 |
val not_Iup_less = thm "not_Iup_less"; |
|
23 |
val not_up_less_UU = thm "not_up_less_UU"; |
|
24 |
val refl_less_up = thm "refl_less_up"; |
|
25 |
val trans_less_up = thm "trans_less_up"; |
|
26 |
val up_chain_cases = thm "up_chain_cases"; |
|
27 |
val up_defined = thm "up_defined"; |
|
28 |
val up_def = thm "up_def"; |
|
29 |
val up_eq = thm "up_eq"; |
|
30 |
val upE = thm "upE"; |
|
31 |
val up_inject = thm "up_inject"; |
|
32 |
val up_lemma1 = thm "up_lemma1"; |
|
33 |
val up_lemma2 = thm "up_lemma2"; |
|
34 |
val up_lemma3 = thm "up_lemma3"; |
|
35 |
val up_lemma4 = thm "up_lemma4"; |
|
36 |
val up_lemma5 = thm "up_lemma5"; |
|
37 |
val up_lemma6 = thm "up_lemma6"; |
|
38 |
val up_less = thm "up_less"; |
|
39 |