isabelle: src/HOLCF/ex/ROOT.ML@ec2a8efd8990 (annotated)

9000 c20d58286a51 cleaned up; wenzelm parents: 6349 diff changeset	1	(* Title: HOLCF/ex/ROOT.ML
244 929fc2c63bd0 HOLCF examples nipkow parents: diff changeset	2
9000 c20d58286a51 cleaned up; wenzelm parents: 6349 diff changeset	3	Misc HOLCF examples.
244 929fc2c63bd0 HOLCF examples nipkow parents: diff changeset	4	*)
929fc2c63bd0 HOLCF examples nipkow parents: diff changeset	5
37110 7ffdbc24b27f move Strict_Fun and Stream theories to new HOLCF/Library directory; add HOLCF/Library to search path huffman parents: 37109 diff changeset	6	use_thys ["Dnat", "Dagstuhl", "Focus_ex", "Fix2", "Hoare",
37000 41a22e7c1145 move some example files into new HOLCF/Tutorial directory huffman parents: 35932 diff changeset	7	"Loop", "Powerdomain_ex", "Domain_Proofs",
35932 86559356502d move letrec stuff to new file HOLCF/ex/Letrec.thy huffman parents: 35167 diff changeset	8	"Letrec",
37110 7ffdbc24b27f move Strict_Fun and Stream theories to new HOLCF/Library directory; add HOLCF/Library to search path huffman parents: 37109 diff changeset	9	"Pattern_Match"];