| author | wenzelm |
| Tue, 14 Jun 2005 22:08:53 +0200 | |
| changeset 16392 | 7212040b71f2 |
| parent 16202 | 61811f31ce5a |
| child 16922 | 2128ac2aa5db |
| permissions | -rw-r--r-- |
|
16202
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset
|
1 |
|
|
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset
|
2 |
(* legacy ML bindings *) |
|
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset
|
3 |
|
|
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset
|
4 |
val less_fun_def = thm "less_fun_def"; |
|
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset
|
5 |
val refl_less_fun = thm "refl_less_fun"; |
|
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset
|
6 |
val antisym_less_fun = thm "antisym_less_fun"; |
|
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset
|
7 |
val trans_less_fun = thm "trans_less_fun"; |
|
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset
|
8 |
val minimal_fun = thm "minimal_fun"; |
|
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset
|
9 |
val least_fun = thm "least_fun"; |
|
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset
|
10 |
val less_fun = thm "less_fun"; |
|
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset
|
11 |
val ch2ch_fun = thm "ch2ch_fun"; |
|
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset
|
12 |
val ub2ub_fun = thm "ub2ub_fun"; |
|
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset
|
13 |
val lub_fun = thm "lub_fun"; |
|
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset
|
14 |
val thelub_fun = thm "thelub_fun"; |
|
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset
|
15 |
val cpo_fun = thm "cpo_fun"; |
|
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset
|
16 |
val inst_fun_pcpo = thm "inst_fun_pcpo"; |