src/HOL/ex/ROOT.ML
author kleing
Sun Feb 12 10:42:19 2006 +0100 (2006-02-12)
changeset 19022 0e6ec4fd204c
parent 18678 dd0c569fa43d
child 19085 a1a251b297dd
permissions -rw-r--r--
* moved ThreeDivides from Isar_examples to better suited HOL/ex
* moved 2 summation lemmas from ThreeDivides to SetInterval
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@12360
     7
time_use_thy "Higher_Order_Logic";
wenzelm@12360
     8
wenzelm@12115
     9
time_use_thy "Recdefs";
paulson@14244
    10
time_use_thy "InductiveInvariant_examples";
wenzelm@12115
    11
time_use_thy "Primrec";
wenzelm@12276
    12
time_use_thy "Locales";
wenzelm@12115
    13
time_use_thy "Records";
wenzelm@12115
    14
time_use_thy "MonoidGroup";
wenzelm@12115
    15
time_use_thy "StringEx";
wenzelm@12115
    16
time_use_thy "BinEx";
wenzelm@12115
    17
setmp proofs 2 time_use_thy "Hilbert_Classical";
wenzelm@12115
    18
time_use_thy "Antiquote";
wenzelm@12115
    19
time_use_thy "Multiquote";
wenzelm@12115
    20
wenzelm@12115
    21
time_use_thy "NatSum";
kleing@19022
    22
time_use_thy "ThreeDivides";
berghofe@12450
    23
time_use_thy "Intuitionistic";
paulson@14220
    24
time_use_thy "Classical";
bauerg@15871
    25
time_use_thy "CTL";
wenzelm@12115
    26
time_use_thy "mesontest2";
berghofe@13880
    27
time_use_thy "PresburgerEx";
chaieb@17378
    28
time_use_thy "Reflected_Presburger";
wenzelm@12115
    29
time_use_thy "BT";
wenzelm@12115
    30
time_use_thy "InSort";
wenzelm@12115
    31
time_use_thy "Qsort";
nipkow@13200
    32
time_use_thy "MergeSort";
wenzelm@12115
    33
time_use_thy "Puzzle";
wenzelm@12115
    34
nipkow@14603
    35
time_use_thy "Lagrange";
chaieb@17378
    36
time_use_thy "Commutative_RingEx";
chaieb@17378
    37
time_use_thy "Commutative_Ring_Complete";
wenzelm@12115
    38
wenzelm@12115
    39
time_use_thy "set";
wenzelm@12115
    40
time_use_thy "MT";
nipkow@14569
    41
nipkow@14569
    42
no_document use_thy "FuncSet";
wenzelm@12115
    43
time_use_thy "Tarski";
wenzelm@12115
    44
wenzelm@12869
    45
time_use_thy "SVC_Oracle";
wenzelm@12115
    46
if_svc_enabled time_use_thy "svc_test";
webertj@14459
    47
webertj@17618
    48
(* requires zChaff with proof generation to be installed: *)
wenzelm@18678
    49
try time_use_thy "SAT_Examples";
webertj@17618
    50
webertj@18408
    51
(* requires zChaff (or some other reasonably fast SAT solver) to be installed: *)
webertj@18408
    52
if getenv "ZCHAFF_HOME" <> "" then
webertj@18408
    53
  time_use_thy "Sudoku"
webertj@18408
    54
else
webertj@18408
    55
  ();
webertj@18408
    56
webertj@14462
    57
time_use_thy "Refute_Examples";
berghofe@14592
    58
time_use_thy "Quickcheck_Examples";
skalberg@14494
    59
nipkow@14569
    60
no_document use_thy "Word";
skalberg@14494
    61
time_use_thy "Adder";
nipkow@14569
    62
wenzelm@17466
    63
HTML.with_charset "utf-8" (no_document time_use_thy) "Hebrew";
wenzelm@17505
    64
HTML.with_charset "utf-8" (no_document time_use_thy) "Chinese";