author | huffman |
Tue, 26 Jul 2005 18:29:59 +0200 | |
changeset 16922 | 2128ac2aa5db |
parent 15576 | efb95d0d01f7 |
child 17838 | 3032e90c4975 |
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 |
|
16922 | 4 |
val dist_eq_one = thms "dist_eq_one"; |
5 |
val dist_less_one = thm "dist_less_one"; |
|
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
6 |
val Exh_one = thm "Exh_one"; |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
7 |
val oneE = thm "oneE"; |