wneuper/isa: src/HOL/ex/ROOT.ML@b1d5b3820d82

     1 (*  Title:      HOL/ex/ROOT.ML

     3 Miscellaneous examples for Higher-Order Logic.

     4 *)

     6 no_document use_thys [

     7   "~~/src/HOL/Library/State_Monad",

     8   "Efficient_Nat_examples",

     9   "~~/src/HOL/Library/FuncSet",

    10   "Eval_Examples",

    11   "Normalization_by_Evaluation",

    12   "Hebrew",

    13   "Chinese",

    14   "Serbian"

    15 ];

    17 use_thys [

    18   "Iff_Oracle",

    19   "Coercion_Examples",

    20   "Numeral",

    21   "Higher_Order_Logic",

    22   "Abstract_NAT",

    23   "Guess",

    24   "Binary",

    25   "Fundefs",

    26   "Induction_Schema",

    27   "LocaleTest2",

    28   "Records",

    29   "While_Combinator_Example",

    30   "MonoidGroup",

    31   "BinEx",

    32   "Hex_Bin_Examples",

    33   "Antiquote",

    34   "Multiquote",

    35   "PER",

    36   "NatSum",

    37   "ThreeDivides",

    38   "Intuitionistic",

    39   "CTL",

    40   "Arith_Examples",

    41   "BT",

    42   "Tree23",

    43   "MergeSort",

    44   "Lagrange",

    45   "Groebner_Examples",

    46   "MT",

    47   "Unification",

    48   "Primrec",

    49   "Tarski",

    50   "Classical",

    51   "Set_Theory",

    52   "Meson_Test",

    53   "Termination",

    54   "Coherent",

    55   "PresburgerEx",

    56   "ReflectionEx",

    57   "Sqrt",

    58   "Sqrt_Script",

    59   "Transfer_Ex",

    60   "Arithmetic_Series_Complex",

    61   "HarmonicSeries",

    62   "Refute_Examples",

    63   "Quickcheck_Examples",

    64   "Quickcheck_Lattice_Examples",

    65   "Landau",

    66   "Execute_Choice",

    67   "Summation",

    68   "Gauge_Integration",

    69   "Dedekind_Real",

    70   "Quicksort",

    71   "Birthday_Paradox",

    72   "List_to_Set_Comprehension_Examples",

    73   "Set_Algebras",

    74   "Seq",

    75   "Simproc_Tests"

    76 ];

    78 if getenv "ISABELLE_GHC" = "" then ()

    79 else use_thy "Quickcheck_Narrowing_Examples";

    81 use_thy "SVC_Oracle";

    82 if getenv "SVC_HOME" = "" then ()

    83 else use_thy "svc_test";

    85 (*requires zChaff (or some other reasonably fast SAT solver)*)

    86 if getenv "ZCHAFF_HOME" = "" then ()

    87 else use_thy "Sudoku";

    89 (*requires a proof-generating SAT solver (zChaff or MiniSAT)*)

    90 (*global side-effects ahead!*)

    91 try use_thy "SAT_Examples";   (* FIXME try!? (not really a proper test) *)

author	huffman
	Fri, 21 Oct 2011 08:42:11 +0200
changeset 46095	b1d5b3820d82
parent 45903	e24bf05dd273
child 47223	f56be74d7f51
permissions	-rw-r--r--