src/HOL/Predicate_Compile_Examples/ROOT.ML
changeset 43938 78a0a2ad91a3
parent 43916 eabe4d6fbd13
equal deleted inserted replaced
43937:768c70befd59 43938:78a0a2ad91a3
     1 use_thys [
     1 use_thys [
     2   "Examples",
     2   "Examples",
     3   "Predicate_Compile_Tests",
     3   "Predicate_Compile_Tests",
     4 (*  "Predicate_Compile_Quickcheck_Examples", -- should be added again soon *)
     4 (*  "Predicate_Compile_Quickcheck_Examples", -- should be added again soon *)
     5   "Specialisation_Examples",
     5   "Specialisation_Examples"
     6 (*  "Hotel_Example_Small_Generator",*)
     6 (*  "Hotel_Example_Small_Generator",
     7   "IMP_1",
     7   "IMP_1",
     8   "IMP_2"
     8   "IMP_2"
     9 (*  "IMP_3",
     9   "IMP_3",
    10   "IMP_4"*)];
    10   "IMP_4"*)];
    11 
    11 
    12 if getenv "ISABELLE_SWIPL" = "" andalso getenv "ISABELLE_YAP" = "" then
    12 if getenv "ISABELLE_SWIPL" = "" andalso getenv "ISABELLE_YAP" = "" then
    13   (warning "No prolog system found - skipping some example theories"; ())
    13   (warning "No prolog system found - skipping some example theories"; ())
    14 else
    14 else