isabelle: src/HOLCF/One.ML@6a1a49cba5b3 (annotated)

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
17838 3032e90c4975 added compactness theorems huffman parents: 16922 diff changeset	4	val compact_ONE = thm "compact_ONE";
16922 2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 15576 diff changeset	5	val dist_eq_one = thms "dist_eq_one";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 15576 diff changeset	6	val dist_less_one = thm "dist_less_one";
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: 14981 diff changeset	7	val Exh_one = thm "Exh_one";
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: 14981 diff changeset	8	val oneE = thm "oneE";