isabelle: src/HOLCF/ROOT.ML@50515882049e (annotated)

3623 e843c1d6f9e1 tuned; wenzelm parents: 3608 diff changeset	1	(* Title: HOLCF/ROOT.ML
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	2	ID: $Id$
1461 6bcb44e4d6e5 expanded tabs clasohm parents: 1361 diff changeset	3	Author: Franz Regensburger
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	4
16841 228d663cc9b3 use all files in HOLCF.thy; wenzelm parents: 16483 diff changeset	5	HOLCF -- a semantic extension of HOL by the LCF logic.
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	6	*)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	7
3623 e843c1d6f9e1 tuned; wenzelm parents: 3608 diff changeset	8	val banner = "HOLCF";
2394 91d8abf108be adaptions for symbol font oheimb parents: 2353 diff changeset	9	writeln banner;
1274 ea0668a1c0ba added 8bit pragmas regensbu parents: 1267 diff changeset	10
ea0668a1c0ba added 8bit pragmas regensbu parents: 1267 diff changeset	11	use_thy "HOLCF";