isabelle: src/HOL/Quickcheck_Examples/ROOT.ML@34e8b7347dda (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",
34e8b7347dda adding theory to prove completeness of the exhaustive generators bulwahn parents: 46701 diff changeset	5	"Completeness"
46585 f462e49eaf11 moving Quickcheck's example to its own session bulwahn parents: diff changeset	6	];
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	if getenv "ISABELLE_GHC" = "" then ()
f462e49eaf11 moving Quickcheck's example to its own session bulwahn parents: diff changeset	9	else use_thy "Quickcheck_Narrowing_Examples";
f462e49eaf11 moving Quickcheck's example to its own session bulwahn parents: diff changeset	10