isabelle: src/HOL/Quickcheck_Examples/ROOT.ML@1f7e068b4613 (annotated)

46585 f462e49eaf11 moving Quickcheck's example to its own session bulwahn parents: diff changeset	1	use_thys [
48415 b42067a3188f restricting Quickcheck_Examples' root file to one basic theory to see if the system error on isatest still occurs bulwahn parents: 48356 diff changeset	2	"Quickcheck_Examples"
b42067a3188f restricting Quickcheck_Examples' root file to one basic theory to see if the system error on isatest still occurs bulwahn parents: 48356 diff changeset	3	(*,
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",
48222 fcca68383808 adding the hotel key card example in Quickcheck-Examples bulwahn parents: 48179 diff changeset	6	"Quickcheck_Interfaces",
48618 1f7e068b4613 moved another larger quickcheck example to Quickcheck_Benchmark bulwahn parents: 48596 diff changeset	7	"Hotel_Example",*)
46585 f462e49eaf11 moving Quickcheck's example to its own session bulwahn parents: diff changeset	8	];
48596 3defa60a7ae3 re-activating Quickcheck_Narrowing_Examples in Quickcheck_Examples bulwahn parents: 48415 diff changeset	9
46585 f462e49eaf11 moving Quickcheck's example to its own session bulwahn parents: diff changeset	10	if getenv "ISABELLE_GHC" = "" then ()
f462e49eaf11 moving Quickcheck's example to its own session bulwahn parents: diff changeset	11	else use_thy "Quickcheck_Narrowing_Examples";
48596 3defa60a7ae3 re-activating Quickcheck_Narrowing_Examples in Quickcheck_Examples bulwahn parents: 48415 diff changeset	12

author	bulwahn
	Thu, 26 Jul 2012 15:55:19 +0200
changeset 48618	1f7e068b4613
parent 48596	3defa60a7ae3
permissions	-rw-r--r--