| author | huffman |
| Fri, 27 May 2005 00:15:24 +0200 | |
| changeset 16092 | a1a481ee9425 |
| parent 15576 | efb95d0d01f7 |
| child 16922 | 2128ac2aa5db |
| permissions | -rw-r--r-- |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
1 |
|
|
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
2 |
(* legacy ML bindings *) |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
3 |
|
|
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
4 |
val Exh_one = thm "Exh_one"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
5 |
val oneE = thm "oneE"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
6 |
val dist_less_one = thm "dist_less_one"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
7 |
val dist_eq_one = thms "dist_eq_one"; |