restricting Quickcheck_Examples' root file to one basic theory to see if the system error on isatest still occurs
authorbulwahn
Sat, 21 Jul 2012 10:55:42 +0200
changeset 49430b42067a3188f
parent 49429 43875bab3a4c
child 49431 5787e1c911d0
restricting Quickcheck_Examples' root file to one basic theory to see if the system error on isatest still occurs
src/HOL/Quickcheck_Examples/ROOT.ML
     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 ()