restricting Quickcheck_Examples' root file to one basic theory to see if the system error on isatest still occurs
1.1 --- a/src/HOL/Quickcheck_Examples/ROOT.ML Sat Jul 21 10:53:26 2012 +0200
1.2 +++ b/src/HOL/Quickcheck_Examples/ROOT.ML Sat Jul 21 10:55:42 2012 +0200
1.3 @@ -1,13 +1,14 @@
1.4 use_thys [
1.5 (* "Find_Unused_Assms_Examples", *)
1.6 - "Quickcheck_Examples",
1.7 + "Quickcheck_Examples"
1.8 + (*,
1.9 "Quickcheck_Lattice_Examples",
1.10 "Completeness",
1.11 "Quickcheck_Interfaces",
1.12 "Hotel_Example",
1.13 "Needham_Schroeder_No_Attacker_Example",
1.14 "Needham_Schroeder_Guided_Attacker_Example",
1.15 - "Needham_Schroeder_Unguided_Attacker_Example"
1.16 + "Needham_Schroeder_Unguided_Attacker_Example"*)
1.17 ];
1.18 (*
1.19 if getenv "ISABELLE_GHC" = "" then ()