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";