isabelle: src/HOL/HOLCF/ex/ROOT.ML@21c42b095c84 (annotated)

42151 4da4fc77664b tuned headers; wenzelm parents: 40774 diff changeset	1	(* Title: HOL/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",
43524 d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis huffman parents: 42151 diff changeset	7	"Concurrency_Monad",
37000 41a22e7c1145 move some example files into new HOLCF/Tutorial directory huffman parents: 35932 diff changeset	8	"Loop", "Powerdomain_ex", "Domain_Proofs",
35932 86559356502d move letrec stuff to new file HOLCF/ex/Letrec.thy huffman parents: 35167 diff changeset	9	"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	10	"Pattern_Match"];