isabelle: src/HOLCF/One.ML@b3846df9d643 (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
16922 2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 15576 diff changeset	4	val dist_eq_one = thms "dist_eq_one";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 15576 diff changeset	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";