src/HOL/ex/ROOT.ML
author wenzelm
Fri Oct 23 20:28:33 1998 +0200 (1998-10-23)
changeset 5753 c90b5f7d0c61
parent 5368 7c8d1c7c876d
child 5866 de6a1856c74a
permissions -rw-r--r--
tuned;
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
clasohm@1165
     9
HOL_build_completed;    (*Cause examples to fail if HOL did*)
clasohm@969
    10
clasohm@1165
    11
writeln "Root file for HOL examples";
wenzelm@4449
    12
set proof_timing;
paulson@3294
    13
wenzelm@5753
    14
(*some examples of recursive function definitions: the TFL package*)
wenzelm@5124
    15
time_use_thy "Recdefs";
paulson@4809
    16
time_use_thy "Primes";
paulson@3294
    17
time_use_thy "Fib";
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@1719
    24
(** time_use "mesontest2.ML";  ULTRA SLOW **)
lcp@1174
    25
time_use_thy "BT";
nipkow@1026
    26
time_use_thy "InSort";
nipkow@1026
    27
time_use_thy "Qsort";
nipkow@1026
    28
time_use_thy "Puzzle";
paulson@3294
    29
paulson@5078
    30
time_use_thy "IntRing";
paulson@5078
    31
clasohm@1351
    32
time_use     "set.ML";
nipkow@1026
    33
time_use_thy "MT";
clasohm@1296
    34
wenzelm@5199
    35
time_use_thy "StringEx";
wenzelm@5199
    36
time_use_thy "BinEx";
wenzelm@5199
    37
wenzelm@5753
    38
(*basic use of extensible records*)
wenzelm@5199
    39
time_use_thy "MonoidGroup";
wenzelm@5753
    40
time_use_thy "Points";
wenzelm@5199
    41
wenzelm@5753
    42
(*groups via locales*)
wenzelm@5250
    43
time_use_thy "PiSets";
wenzelm@5250
    44
time_use_thy "LocaleGroup";
wenzelm@5250
    45
wenzelm@5753
    46
(*expressions with quote / antiquote syntax*)
wenzelm@5368
    47
time_use_thy "Antiquote";
wenzelm@5368
    48
wenzelm@5199
    49
clasohm@1165
    50
writeln "END: Root file for HOL examples";