wenzelm@12115: (*  Title:      HOL/ex/ROOT.ML
wenzelm@11586: 
wenzelm@12115: Miscellaneous examples for Higher-Order Logic.
wenzelm@12115: *)
wenzelm@12115: 
wenzelm@24528: no_document use_thys [
wenzelm@24740:   "State_Monad",
haftmann@25963:   "Efficient_Nat_examples",
haftmann@25963:   "FuncSet",
haftmann@25963:   "Word",
haftmann@25963:   "Eval_Examples",
haftmann@31378:   "Codegenerator_Test",
haftmann@31378:   "Codegenerator_Pretty_Test",
wenzelm@29377:   "NormalForm",
haftmann@31129:   "Predicate_Compile",
bulwahn@33651:   "Predicate_Compile_ex",
bulwahn@33651:   "Predicate_Compile_Quickcheck"
haftmann@25963: ];
haftmann@25963: 
wenzelm@24478: use_thys [
haftmann@28021:   "Numeral",
wenzelm@24478:   "Higher_Order_Logic",
wenzelm@24478:   "Abstract_NAT",
wenzelm@24478:   "Guess",
wenzelm@24478:   "Binary",
wenzelm@24478:   "Recdefs",
wenzelm@24478:   "Fundefs",
krauss@33471:   "Induction_Schema",
wenzelm@24478:   "InductiveInvariant_examples",
wenzelm@24478:   "LocaleTest2",
wenzelm@24478:   "Records",
wenzelm@24478:   "MonoidGroup",
wenzelm@24478:   "BinEx",
wenzelm@24478:   "Hex_Bin_Examples",
wenzelm@24478:   "Antiquote",
wenzelm@24478:   "Multiquote",
wenzelm@24478:   "PER",
wenzelm@24478:   "NatSum",
wenzelm@24478:   "ThreeDivides",
wenzelm@24478:   "Intuitionistic",
wenzelm@24478:   "CTL",
wenzelm@24478:   "Arith_Examples",
wenzelm@24478:   "BT",
nipkow@33425:   "Tree23",
wenzelm@24478:   "MergeSort",
wenzelm@24478:   "Lagrange",
wenzelm@24478:   "Groebner_Examples",
wenzelm@24478:   "MT",
wenzelm@24478:   "Unification",
wenzelm@24740:   "Primrec",
wenzelm@24740:   "Tarski",
wenzelm@25738:   "Adder",
wenzelm@25738:   "Classical",
wenzelm@25738:   "set",
haftmann@27436:   "Meson_Test",
krauss@29181:   "Termination",
wenzelm@29376:   "Coherent",
wenzelm@29376:   "PresburgerEx",
wenzelm@29377:   "ReflectionEx",
wenzelm@29377:   "BinEx",
wenzelm@29377:   "Sqrt",
wenzelm@29377:   "Sqrt_Script",
haftmann@32560:   "Transfer_Ex",
wenzelm@29377:   "Arithmetic_Series_Complex",
wenzelm@29377:   "HarmonicSeries",
wenzelm@29377:   "Refute_Examples",
chaieb@29697:   "Quickcheck_Examples",
haftmann@35160:   "Landau",
haftmann@35163:   "Execute_Choice",
haftmann@35163:   "Summation"
wenzelm@24478: ];
wenzelm@21256: 
wenzelm@33546: HTML.with_charset "utf-8" (no_document use_thys)
wenzelm@33546:   ["Hebrew", "Chinese", "Serbian"];
wenzelm@33546: 
wenzelm@32615: (setmp_noncritical proofs 2 (setmp_noncritical Goal.parallel_proofs 0 use_thy))
wenzelm@32260:   "Hilbert_Classical";
wenzelm@24478: 
wenzelm@32428: use_thy "SVC_Oracle";
wenzelm@32428: if getenv "SVC_HOME" = "" then ()
wenzelm@32428: else use_thy "svc_test";
wenzelm@12115: 
wenzelm@32428: (*requires zChaff (or some other reasonably fast SAT solver)*)
wenzelm@32428: if getenv "ZCHAFF_HOME" = "" then ()
wenzelm@32428: else use_thy "Sudoku";
webertj@18408: 
wenzelm@33546: (*requires a proof-generating SAT solver (zChaff or MiniSAT)*)
wenzelm@33546: (*global side-effects ahead!*)
wenzelm@33546: try use_thy "SAT_Examples";   (* FIXME try!? (not really a proper test) *)