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@41661:   "~~/src/HOL/Library/State_Monad",
haftmann@25963:   "Efficient_Nat_examples",
wenzelm@41661:   "~~/src/HOL/Library/FuncSet",
haftmann@25963:   "Eval_Examples",
wenzelm@41194:   "Normalization_by_Evaluation",
wenzelm@41194:   "Hebrew",
wenzelm@41194:   "Chinese",
wenzelm@41194:   "Serbian"
haftmann@25963: ];
haftmann@25963: 
wenzelm@24478: use_thys [
wenzelm@40495:   "Iff_Oracle",
wenzelm@40528:   "Coercion_Examples",
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",
krauss@37759:   "While_Combinator_Example",
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:   "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",
bulwahn@38157:   "Quickcheck_Lattice_Examples",
haftmann@35160:   "Landau",
haftmann@35163:   "Execute_Choice",
hoelzl@35328:   "Summation",
huffman@36787:   "Gauge_Integration",
haftmann@40590:   "Dedekind_Real",
bulwahn@40880:   "Quicksort",
bulwahn@41697:   "Birthday_Paradoxon",
haftmann@41829:   "List_to_Set_Comprehension_Examples",
bulwahn@42785:   "Set_Algebras"
wenzelm@24478: ];
wenzelm@21256: 
bulwahn@42785: if getenv "EXEC_GHC" = "" then ()
bulwahn@42785: else use_thy "LSC_Examples";
bulwahn@42785: 
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) *)