1.1 --- a/src/HOL/Predicate_Compile_Examples/ROOT.ML	Thu Jul 21 08:31:35 2011 +0200
     1.2 +++ b/src/HOL/Predicate_Compile_Examples/ROOT.ML	Thu Jul 21 08:33:57 2011 +0200
     1.3 @@ -2,11 +2,11 @@
     1.4    "Examples",
     1.5    "Predicate_Compile_Tests",
     1.6  (*  "Predicate_Compile_Quickcheck_Examples", -- should be added again soon *)
     1.7 -  "Specialisation_Examples",
     1.8 -(*  "Hotel_Example_Small_Generator",*)
     1.9 +  "Specialisation_Examples"
    1.10 +(*  "Hotel_Example_Small_Generator",
    1.11    "IMP_1",
    1.12    "IMP_2"
    1.13 -(*  "IMP_3",
    1.14 +  "IMP_3",
    1.15    "IMP_4"*)];
    1.16  
    1.17  if getenv "ISABELLE_SWIPL" = "" andalso getenv "ISABELLE_YAP" = "" then