src/HOL/Predicate_Compile_Examples/ROOT.ML
author wenzelm
Fri Dec 17 17:43:54 2010 +0100 (2010-12-17)
changeset 41229 d797baa3d57c
parent 40243 3102b27ca03a
child 41952 c7297638599b
permissions -rw-r--r--
replaced command 'nonterminals' by slightly modernized version 'nonterminal';
wenzelm@39616
     1
use_thys [
bulwahn@39655
     2
  "Examples",
bulwahn@39655
     3
  "Predicate_Compile_Tests",
bulwahn@40055
     4
(*  "Predicate_Compile_Quickcheck_Examples", -- should be added again soon *)
wenzelm@39616
     5
  "Specialisation_Examples",
bulwahn@40104
     6
  "Hotel_Example_Small_Generator",
wenzelm@39616
     7
  "IMP_1",
bulwahn@40137
     8
  "IMP_2"
bulwahn@40137
     9
(*  "IMP_3",
bulwahn@40137
    10
  "IMP_4"*)];
wenzelm@39616
    11
bulwahn@39544
    12
if getenv "EXEC_SWIPL" = "" andalso getenv "EXEC_YAP" = "" then
wenzelm@39616
    13
  (warning "No prolog system found - skipping some example theories"; ())
bulwahn@39544
    14
else
bulwahn@40243
    15
  if not (getenv "EXEC_SWIPL" = "") orelse (getenv "SWIPL_VERSION" = "5.10.1") then
bulwahn@40243
    16
     (use_thys [
bulwahn@40243
    17
        "Code_Prolog_Examples",
bulwahn@40243
    18
        "Context_Free_Grammar_Example",
bulwahn@40243
    19
        "Hotel_Example_Prolog",
bulwahn@40243
    20
        "Lambda_Example",
bulwahn@40243
    21
        "List_Examples"];
bulwahn@40243
    22
      Unsynchronized.setmp quick_and_dirty true use_thys ["Reg_Exp_Example"])
bulwahn@40243
    23
    else (warning "Unsupported SWI-Prolog version - skipping some example theories"; ());