src/HOL/Predicate_Compile_Examples/ROOT.ML
author blanchet
Wed, 15 Dec 2010 18:10:32 +0100
changeset 41171 043f8dc3b51f
parent 40243 3102b27ca03a
child 41952 c7297638599b
permissions -rw-r--r--
facilitate debugging

use_thys [
  "Examples",
  "Predicate_Compile_Tests",
(*  "Predicate_Compile_Quickcheck_Examples", -- should be added again soon *)
  "Specialisation_Examples",
  "Hotel_Example_Small_Generator",
  "IMP_1",
  "IMP_2"
(*  "IMP_3",
  "IMP_4"*)];

if getenv "EXEC_SWIPL" = "" andalso getenv "EXEC_YAP" = "" then
  (warning "No prolog system found - skipping some example theories"; ())
else
  if not (getenv "EXEC_SWIPL" = "") orelse (getenv "SWIPL_VERSION" = "5.10.1") then
     (use_thys [
        "Code_Prolog_Examples",
        "Context_Free_Grammar_Example",
        "Hotel_Example_Prolog",
        "Lambda_Example",
        "List_Examples"];
      Unsynchronized.setmp quick_and_dirty true use_thys ["Reg_Exp_Example"])
    else (warning "Unsupported SWI-Prolog version - skipping some example theories"; ());