src/HOL/ex/ROOT.ML
author nipkow
Fri May 05 12:51:33 2000 +0200 (2000-05-05)
changeset 8797 b55e2354d71e
parent 8569 748a9699f28d
child 8933 de96f2982d2c
permissions -rw-r--r--
Added AVL
clasohm@1465
     1
(*  Title:      HOL/ex/ROOT
clasohm@969
     2
    ID:         $Id$
clasohm@1465
     3
    Author:     Tobias Nipkow, Cambridge University Computer Laboratory
clasohm@969
     4
    Copyright   1991  University of Cambridge
clasohm@969
     5
clasohm@969
     6
Executes miscellaneous examples for Higher-Order Logic. 
clasohm@969
     7
*)
clasohm@969
     8
wenzelm@6349
     9
writeln "Root file for HOL examples";
clasohm@969
    10
wenzelm@4449
    11
set proof_timing;
paulson@3294
    12
wenzelm@5753
    13
(*some examples of recursive function definitions: the TFL package*)
wenzelm@5124
    14
time_use_thy "Recdefs";
paulson@4809
    15
time_use_thy "Primes";
paulson@3294
    16
time_use_thy "Fib";
paulson@8353
    17
with_path "../Induct" use_thy "Factorization";
paulson@3337
    18
time_use_thy "Primrec";
paulson@3294
    19
paulson@3294
    20
time_use_thy "NatSum";
clasohm@1351
    21
time_use     "cla.ML";
clasohm@1351
    22
time_use     "meson.ML";
clasohm@1351
    23
time_use     "mesontest.ML";
paulson@8557
    24
time_use     "mesontest2.ML";
lcp@1174
    25
time_use_thy "BT";
nipkow@8797
    26
time_use_thy "AVL";
nipkow@1026
    27
time_use_thy "InSort";
nipkow@1026
    28
time_use_thy "Qsort";
nipkow@1026
    29
time_use_thy "Puzzle";
paulson@3294
    30
paulson@5078
    31
time_use_thy "IntRing";
paulson@5078
    32
clasohm@1351
    33
time_use     "set.ML";
nipkow@1026
    34
time_use_thy "MT";
paulson@7085
    35
time_use_thy "Tarski";
clasohm@1296
    36
wenzelm@5199
    37
time_use_thy "StringEx";
wenzelm@5199
    38
time_use_thy "BinEx";
paulson@7187
    39
wenzelm@7304
    40
if_svc_enabled time_use_thy "svc_test";
wenzelm@5199
    41
wenzelm@5753
    42
(*basic use of extensible records*)
wenzelm@5199
    43
time_use_thy "MonoidGroup";
wenzelm@5753
    44
time_use_thy "Points";
wenzelm@5199
    45
wenzelm@5753
    46
(*groups via locales*)
wenzelm@5250
    47
time_use_thy "PiSets";
wenzelm@5250
    48
time_use_thy "LocaleGroup";
wenzelm@5250
    49
wenzelm@5753
    50
(*expressions with quote / antiquote syntax*)
wenzelm@5368
    51
time_use_thy "Antiquote";
wenzelm@8569
    52
time_use_thy "Multiquote";
wenzelm@5368
    53
wenzelm@5199
    54
clasohm@1165
    55
writeln "END: Root file for HOL examples";