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

46585 f462e49eaf11 moving Quickcheck's example to its own session bulwahn parents: diff changeset	1	use_thys [
48267 f5676fad35a3 deactivate Find_Unused_Assms_Examples to see if isabelle test's failures is caused by this example file bulwahn parents: 48243 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",
48222 fcca68383808 adding the hotel key card example in Quickcheck-Examples bulwahn parents: 48179 diff changeset	6	"Quickcheck_Interfaces",
48224 f2dd90cc724b adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck) bulwahn parents: 48222 diff changeset	7	"Hotel_Example",
48243 b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck bulwahn parents: 48224 diff changeset	8	"Needham_Schroeder_No_Attacker_Example",
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck bulwahn parents: 48224 diff changeset	9	"Needham_Schroeder_Guided_Attacker_Example",
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck bulwahn parents: 48224 diff changeset	10	"Needham_Schroeder_Unguided_Attacker_Example"
46585 f462e49eaf11 moving Quickcheck's example to its own session bulwahn parents: diff changeset	11	];
f462e49eaf11 moving Quickcheck's example to its own session bulwahn parents: diff changeset	12
f462e49eaf11 moving Quickcheck's example to its own session bulwahn parents: diff changeset	13	if getenv "ISABELLE_GHC" = "" then ()
f462e49eaf11 moving Quickcheck's example to its own session bulwahn parents: diff changeset	14	else use_thy "Quickcheck_Narrowing_Examples";
f462e49eaf11 moving Quickcheck's example to its own session bulwahn parents: diff changeset	15

author	bulwahn
	Mon, 16 Jul 2012 08:44:29 +0200
changeset 48267	f5676fad35a3
parent 48243	b149de01d669
child 48356	b6081af563a9
permissions	-rw-r--r--