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';
     1 use_thys [
     2   "Examples",
     3   "Predicate_Compile_Tests",
     4 (*  "Predicate_Compile_Quickcheck_Examples", -- should be added again soon *)
     5   "Specialisation_Examples",
     6   "Hotel_Example_Small_Generator",
     7   "IMP_1",
     8   "IMP_2"
     9 (*  "IMP_3",
    10   "IMP_4"*)];
    11 
    12 if getenv "EXEC_SWIPL" = "" andalso getenv "EXEC_YAP" = "" then
    13   (warning "No prolog system found - skipping some example theories"; ())
    14 else
    15   if not (getenv "EXEC_SWIPL" = "") orelse (getenv "SWIPL_VERSION" = "5.10.1") then
    16      (use_thys [
    17         "Code_Prolog_Examples",
    18         "Context_Free_Grammar_Example",
    19         "Hotel_Example_Prolog",
    20         "Lambda_Example",
    21         "List_Examples"];
    22       Unsynchronized.setmp quick_and_dirty true use_thys ["Reg_Exp_Example"])
    23     else (warning "Unsupported SWI-Prolog version - skipping some example theories"; ());