src/HOL/ex/ROOT.ML
changeset 47456 f462e49eaf11
parent 47426 fdb84c40e074
child 47978 2a1953f0d20d
     1.1 --- a/src/HOL/ex/ROOT.ML	Tue Feb 21 23:25:36 2012 +0100
     1.2 +++ b/src/HOL/ex/ROOT.ML	Wed Feb 22 08:01:41 2012 +0100
     1.3 @@ -60,8 +60,6 @@
     1.4    "Arithmetic_Series_Complex",
     1.5    "HarmonicSeries",
     1.6    "Refute_Examples",
     1.7 -  "Quickcheck_Examples",
     1.8 -  "Quickcheck_Lattice_Examples",
     1.9    "Landau",
    1.10    "Execute_Choice",
    1.11    "Summation",
    1.12 @@ -76,9 +74,6 @@
    1.13    "Executable_Relation"
    1.14  ];
    1.15  
    1.16 -if getenv "ISABELLE_GHC" = "" then ()
    1.17 -else use_thy "Quickcheck_Narrowing_Examples";
    1.18 -
    1.19  use_thy "SVC_Oracle";
    1.20  if getenv "SVC_HOME" = "" then ()
    1.21  else use_thy "svc_test";