src/HOL/ex/ROOT.ML
author wenzelm
Wed, 02 Jun 2010 13:18:21 +0200
changeset 37280 0fb011773adc
parent 36962 5fb251d1c32f
child 37695 71e84a203c19
permissions -rw-r--r--
Hilbert_Classical: disable multithreading altogether, otherwise proof normalization will fork futures independently of Goal.parallel_proofs;

(*  Title:      HOL/ex/ROOT.ML

Miscellaneous examples for Higher-Order Logic.
*)

no_document use_thys [
  "State_Monad",
  "Efficient_Nat_examples",
  "FuncSet",
  "Eval_Examples",
  "Codegenerator_Test",
  "Codegenerator_Pretty_Test",
  "NormalForm"
];

use_thys [
  "Numeral",
  "Higher_Order_Logic",
  "Abstract_NAT",
  "Guess",
  "Binary",
  "Recdefs",
  "Fundefs",
  "Induction_Schema",
  "InductiveInvariant_examples",
  "LocaleTest2",
  "Records",
  "MonoidGroup",
  "BinEx",
  "Hex_Bin_Examples",
  "Antiquote",
  "Multiquote",
  "PER",
  "NatSum",
  "ThreeDivides",
  "Intuitionistic",
  "CTL",
  "Arith_Examples",
  "BT",
  "Tree23",
  "MergeSort",
  "Lagrange",
  "Groebner_Examples",
  "MT",
  "Unification",
  "Primrec",
  "Tarski",
  "Classical",
  "set",
  "Meson_Test",
  "Termination",
  "Coherent",
  "PresburgerEx",
  "ReflectionEx",
  "BinEx",
  "Sqrt",
  "Sqrt_Script",
  "Transfer_Ex",
  "Arithmetic_Series_Complex",
  "HarmonicSeries",
  "Refute_Examples",
  "Quickcheck_Examples",
  "Landau",
  "Execute_Choice",
  "Summation",
  "Gauge_Integration",
  "Dedekind_Real"
];

HTML.with_charset "utf-8" (no_document use_thys)
  ["Hebrew", "Chinese", "Serbian"];

(setmp_noncritical proofs 2 (setmp_noncritical Multithreading.max_threads 1 use_thy))
  "Hilbert_Classical";

use_thy "SVC_Oracle";
if getenv "SVC_HOME" = "" then ()
else use_thy "svc_test";

(*requires zChaff (or some other reasonably fast SAT solver)*)
if getenv "ZCHAFF_HOME" = "" then ()
else use_thy "Sudoku";

(*requires a proof-generating SAT solver (zChaff or MiniSAT)*)
(*global side-effects ahead!*)
try use_thy "SAT_Examples";   (* FIXME try!? (not really a proper test) *)