src/HOLCF/One.ML
author huffman
Sat, 04 Jun 2005 00:22:08 +0200
changeset 16221 879400e029bf
parent 15576 efb95d0d01f7
child 16922 2128ac2aa5db
permissions -rw-r--r--
New theory with lemmas for the fixrec package
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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";