src/HOL/ex/ROOT.ML
author wenzelm
Fri Aug 20 15:41:53 1999 +0200 (1999-08-20)
changeset 7304 94c6f8f07631
parent 7187 676027b1d770
child 8353 57a163920480
permissions -rw-r--r--
if_svc_enabled;
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@3337
    17
time_use_thy "Primrec";
paulson@3294
    18
paulson@3294
    19
time_use_thy "NatSum";
clasohm@1351
    20
time_use     "cla.ML";
clasohm@1351
    21
time_use     "meson.ML";
clasohm@1351
    22
time_use     "mesontest.ML";
lcp@1174
    23
time_use_thy "BT";
nipkow@1026
    24
time_use_thy "InSort";
nipkow@1026
    25
time_use_thy "Qsort";
nipkow@1026
    26
time_use_thy "Puzzle";
paulson@3294
    27
paulson@5078
    28
time_use_thy "IntRing";
paulson@5078
    29
clasohm@1351
    30
time_use     "set.ML";
nipkow@1026
    31
time_use_thy "MT";
paulson@7085
    32
time_use_thy "Tarski";
clasohm@1296
    33
wenzelm@5199
    34
time_use_thy "StringEx";
wenzelm@5199
    35
time_use_thy "BinEx";
paulson@7187
    36
wenzelm@7304
    37
if_svc_enabled time_use_thy "svc_test";
wenzelm@5199
    38
wenzelm@5753
    39
(*basic use of extensible records*)
wenzelm@5199
    40
time_use_thy "MonoidGroup";
wenzelm@5753
    41
time_use_thy "Points";
wenzelm@5199
    42
wenzelm@5753
    43
(*groups via locales*)
wenzelm@5250
    44
time_use_thy "PiSets";
wenzelm@5250
    45
time_use_thy "LocaleGroup";
wenzelm@5250
    46
wenzelm@5753
    47
(*expressions with quote / antiquote syntax*)
wenzelm@5368
    48
time_use_thy "Antiquote";
wenzelm@5368
    49
wenzelm@5199
    50
clasohm@1165
    51
writeln "END: Root file for HOL examples";