isabelle: src/HOL/Quickcheck_Examples/ROOT.ML@18461f745b4a (annotated)

46585 f462e49eaf11 moving Quickcheck's example to its own session bulwahn parents: diff changeset	1	use_thys [
46701 879f5c76ffb6 reactivated Find_Unused_Assms_Examples to avoid untested / dead stuff in the repository; wenzelm parents: 46697 diff changeset	2	"Find_Unused_Assms_Examples",
46585 f462e49eaf11 moving Quickcheck's example to its own session bulwahn parents: diff changeset	3	"Quickcheck_Examples",
47205 34e8b7347dda adding theory to prove completeness of the exhaustive generators bulwahn parents: 46701 diff changeset	4	"Quickcheck_Lattice_Examples",
48179 18461f745b4a adding some minimal documentation and an example of quickcheck's interfaces bulwahn parents: 47205 diff changeset	5	"Completeness",
18461f745b4a adding some minimal documentation and an example of quickcheck's interfaces bulwahn parents: 47205 diff changeset	6	"Quickcheck_Interfaces"
46585 f462e49eaf11 moving Quickcheck's example to its own session bulwahn parents: diff changeset	7	];
f462e49eaf11 moving Quickcheck's example to its own session bulwahn parents: diff changeset	8
f462e49eaf11 moving Quickcheck's example to its own session bulwahn parents: diff changeset	9	if getenv "ISABELLE_GHC" = "" then ()
f462e49eaf11 moving Quickcheck's example to its own session bulwahn parents: diff changeset	10	else use_thy "Quickcheck_Narrowing_Examples";
f462e49eaf11 moving Quickcheck's example to its own session bulwahn parents: diff changeset	11