# HG changeset patch
# User bulwahn
# Date 1342860942 -7200
# Node ID b42067a3188fd2cc0947383f23aabfb06159d967
# Parent  43875bab3a4cb65d82298475cff375fe360618a5
restricting Quickcheck_Examples' root file to one basic theory to see if the system error on isatest still occurs

diff -r 43875bab3a4c -r b42067a3188f src/HOL/Quickcheck_Examples/ROOT.ML
--- 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 ()