restricting Quickcheck_Examples' root file to one basic theory to see if the system error on isatest still occurs
--- a/src/HOL/Quickcheck_Examples/ROOT.ML Sat Jul 21 10:53:26 2012 +0200
+++ b/src/HOL/Quickcheck_Examples/ROOT.ML Sat Jul 21 10:55:42 2012 +0200
@@ -1,13 +1,14 @@
use_thys [
(* "Find_Unused_Assms_Examples", *)
- "Quickcheck_Examples",
+ "Quickcheck_Examples"
+ (*,
"Quickcheck_Lattice_Examples",
"Completeness",
"Quickcheck_Interfaces",
"Hotel_Example",
"Needham_Schroeder_No_Attacker_Example",
"Needham_Schroeder_Guided_Attacker_Example",
- "Needham_Schroeder_Unguided_Attacker_Example"
+ "Needham_Schroeder_Unguided_Attacker_Example"*)
];
(*
if getenv "ISABELLE_GHC" = "" then ()