isabelle: src/HOLCF/ex/ROOT.ML@6e969ce3dfcc (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
24106 f2965bf954dc simultaneous use_thys; wenzelm parents: 18072 diff changeset	6	use_thys ["Dnat", "Stream", "Dagstuhl", "Focus_ex", "Fix2", "Hoare",
33813 0bc8d4f786bd example theory for new domain package huffman parents: 33591 diff changeset	7	"Loop", "Fixrec_ex", "Powerdomain_ex", "Domain_ex", "Domain_Proofs",
35932 86559356502d move letrec stuff to new file HOLCF/ex/Letrec.thy huffman parents: 35167 diff changeset	8	"Letrec",
35167 eba22d68a0a7 add theory HOLCF/ex/Strict_Fun.thy huffman parents: 33813 diff changeset	9	"Strict_Fun",
33813 0bc8d4f786bd example theory for new domain package huffman parents: 33591 diff changeset	10	"New_Domain"];