| author | huffman |
| Fri, 08 Jul 2005 02:41:19 +0200 | |
| changeset 16753 | fb6801c926d2 |
| parent 16319 | 1ff2965cc2e7 |
| child 16922 | 2128ac2aa5db |
| 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 less_up_def = thm "less_up_def"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
5 |
val refl_less_up = thm "refl_less_up"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
6 |
val antisym_less_up = thm "antisym_less_up"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
7 |
val trans_less_up = thm "trans_less_up"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
8 |
val minimal_up = thm "minimal_up"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
9 |
val least_up = thm "least_up"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
10 |
val monofun_Ifup2 = thm "monofun_Ifup2"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
11 |
val up_lemma1 = thm "up_lemma1"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
12 |
val cpo_up = thm "cpo_up"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
13 |
val up_def = thm "up_def"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
14 |
val fup_def = thm "fup_def"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
15 |
val inst_up_pcpo = thm "inst_up_pcpo"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
16 |
val cont_Iup = thm "cont_Iup"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
17 |
val cont_Ifup1 = thm "cont_Ifup1"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
18 |
val cont_Ifup2 = thm "cont_Ifup2"; |
| 16753 | 19 |
val Exh_Up = thm "Exh_Up"; |
|
16319
1ff2965cc2e7
major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents:
15576
diff
changeset
|
20 |
val up_inject = thm "up_inject"; |
|
1ff2965cc2e7
major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents:
15576
diff
changeset
|
21 |
val up_eq = thm "up_eq"; |
|
1ff2965cc2e7
major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents:
15576
diff
changeset
|
22 |
val up_defined = thm "up_defined"; |
|
1ff2965cc2e7
major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents:
15576
diff
changeset
|
23 |
val up_less = thm "up_less"; |
| 16753 | 24 |
val upE = thm "upE"; |
|
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
25 |
val fup1 = thm "fup1"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
26 |
val fup2 = thm "fup2"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
27 |
val fup3 = thm "fup3"; |