isabelle: src/HOLCF/HOLCF.ML@a0e3f2df9b0e (annotated)

1461 6bcb44e4d6e5 expanded tabs clasohm parents: 1274 diff changeset	1	(* Title: HOLCF/HOLCF.ML
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	2	ID: $Id$
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	3	*)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	4
15650 b37dc98fbbc5 converted to new-style theory huffman parents: 14981 diff changeset	5	structure HOLCF =
b37dc98fbbc5 converted to new-style theory huffman parents: 14981 diff changeset	6	struct
b37dc98fbbc5 converted to new-style theory huffman parents: 14981 diff changeset	7	val thy = the_context ();
b37dc98fbbc5 converted to new-style theory huffman parents: 14981 diff changeset	8	end;