isabelle: src/HOL/HOLCF/ROOT.ML@233f30abb040 (annotated)

42151 4da4fc77664b tuned headers; wenzelm parents: 41413 diff changeset	1	(* Title: HOL/HOLCF/ROOT.ML
1461 6bcb44e4d6e5 expanded tabs clasohm parents: 1361 diff changeset	2	Author: Franz Regensburger
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	3
16841 228d663cc9b3 use all files in HOLCF.thy; wenzelm parents: 16483 diff changeset	4	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	5	*)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	6
41413 64cd30d6b0b8 explicit file specifications -- avoid secondary load path; wenzelm parents: 40774 diff changeset	7	no_document use_thys ["~~/src/HOL/Library/Nat_Bijection", "~~/src/HOL/Library/Countable"];
29921 3d50e96bcd6b fixed document nipkow parents: 22707 diff changeset	8
40505 702708d26c9b reorder chapters for generated document huffman parents: 39982 diff changeset	9	use_thys ["Plain_HOLCF", "Fixrec", "HOLCF"];