src/HOL/ex/ROOT.ML
author urbanc
Tue Jun 05 09:56:19 2007 +0200 (2007-06-05)
changeset 23243 a37d3e6e8323
parent 23193 1f2d94b6a8ef
child 23271 3f9ef4bf3f31
permissions -rw-r--r--
included Class.thy in the compiling process for Nominal/Examples
wenzelm@12115
     1
(*  Title:      HOL/ex/ROOT.ML
wenzelm@12115
     2
    ID:         $Id$
wenzelm@11586
     3
wenzelm@12115
     4
Miscellaneous examples for Higher-Order Logic.
wenzelm@12115
     5
*)
wenzelm@12115
     6
wenzelm@21256
     7
no_document use_thy "Parity";
wenzelm@21256
     8
no_document use_thy "GCD";
wenzelm@21256
     9
wenzelm@19438
    10
no_document time_use_thy "Classpackage";
haftmann@22522
    11
no_document time_use_thy "Eval_examples";
haftmann@22528
    12
no_document time_use_thy "Random";
haftmann@22067
    13
no_document time_use_thy "Codegenerator_Rat";
haftmann@21911
    14
no_document time_use_thy "Codegenerator";
wenzelm@19438
    15
wenzelm@12360
    16
time_use_thy "Higher_Order_Logic";
wenzelm@19085
    17
time_use_thy "Abstract_NAT";
wenzelm@19997
    18
time_use_thy "Guess";
wenzelm@22140
    19
time_use_thy "Binary";
wenzelm@12360
    20
wenzelm@12115
    21
time_use_thy "Recdefs";
krauss@22167
    22
time_use_thy "Fundefs";
paulson@14244
    23
time_use_thy "InductiveInvariant_examples";
wenzelm@12115
    24
time_use_thy "Primrec";
wenzelm@12276
    25
time_use_thy "Locales";
ballarin@22657
    26
time_use_thy "LocaleTest2";
wenzelm@12115
    27
time_use_thy "Records";
wenzelm@12115
    28
time_use_thy "MonoidGroup";
wenzelm@12115
    29
time_use_thy "BinEx";
kleing@20866
    30
time_use_thy "Hex_Bin_Examples";
wenzelm@12115
    31
setmp proofs 2 time_use_thy "Hilbert_Classical";
wenzelm@12115
    32
time_use_thy "Antiquote";
wenzelm@12115
    33
time_use_thy "Multiquote";
wenzelm@12115
    34
wenzelm@20812
    35
time_use_thy "PER";
wenzelm@12115
    36
time_use_thy "NatSum";
kleing@19022
    37
time_use_thy "ThreeDivides";
berghofe@12450
    38
time_use_thy "Intuitionistic";
paulson@14220
    39
time_use_thy "Classical";
bauerg@15871
    40
time_use_thy "CTL";
wenzelm@12115
    41
time_use_thy "mesontest2";
webertj@23193
    42
time_use_thy "Arith_Examples";
berghofe@13880
    43
time_use_thy "PresburgerEx";
chaieb@17378
    44
time_use_thy "Reflected_Presburger";
wenzelm@12115
    45
time_use_thy "BT";
wenzelm@12115
    46
time_use_thy "InSort";
wenzelm@12115
    47
time_use_thy "Qsort";
nipkow@13200
    48
time_use_thy "MergeSort";
wenzelm@12115
    49
time_use_thy "Puzzle";
wenzelm@12115
    50
nipkow@14603
    51
time_use_thy "Lagrange";
chaieb@17378
    52
time_use_thy "Commutative_RingEx";
chaieb@17378
    53
time_use_thy "Commutative_Ring_Complete";
wenzelm@20325
    54
time_use_thy "Reflection";
wenzelm@12115
    55
wenzelm@12115
    56
time_use_thy "set";
wenzelm@12115
    57
time_use_thy "MT";
nipkow@14569
    58
nipkow@14569
    59
no_document use_thy "FuncSet";
wenzelm@12115
    60
time_use_thy "Tarski";
wenzelm@12115
    61
wenzelm@12869
    62
time_use_thy "SVC_Oracle";
wenzelm@12115
    63
if_svc_enabled time_use_thy "svc_test";
webertj@14459
    64
webertj@23191
    65
(* requires a proof-generating SAT solver (zChaff or MiniSAT) to be *)
webertj@23191
    66
(* installed:                                                       *)
wenzelm@18678
    67
try time_use_thy "SAT_Examples";
webertj@17618
    68
webertj@23191
    69
(* requires zChaff (or some other reasonably fast SAT solver) to be *)
webertj@23191
    70
(* installed:                                                       *)
webertj@18408
    71
if getenv "ZCHAFF_HOME" <> "" then
webertj@18408
    72
  time_use_thy "Sudoku"
webertj@23191
    73
else ();
webertj@18408
    74
webertj@14462
    75
time_use_thy "Refute_Examples";
berghofe@14592
    76
time_use_thy "Quickcheck_Examples";
nipkow@19832
    77
no_document time_use_thy "NormalForm";
skalberg@14494
    78
nipkow@14569
    79
no_document use_thy "Word";
skalberg@14494
    80
time_use_thy "Adder";
nipkow@14569
    81
wenzelm@17466
    82
HTML.with_charset "utf-8" (no_document time_use_thy) "Hebrew";
wenzelm@17505
    83
HTML.with_charset "utf-8" (no_document time_use_thy) "Chinese";
krauss@22999
    84
krauss@22999
    85
time_use_thy "Unification";