src/HOL/ex/ROOT.ML
author wenzelm
Wed Jun 21 15:58:23 2000 +0200 (2000-06-21)
changeset 9100 9e081c812338
parent 9000 c20d58286a51
child 9297 bafe45732b10
permissions -rw-r--r--
fixed deps;
wenzelm@9000
     1
(*  Title:      HOL/ex/ROOT.ML
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@5753
     9
(*some examples of recursive function definitions: the TFL package*)
wenzelm@5124
    10
time_use_thy "Recdefs";
paulson@4809
    11
time_use_thy "Primes";
paulson@3294
    12
time_use_thy "Fib";
wenzelm@9000
    13
with_path "../Induct" time_use_thy "Factorization";
paulson@3337
    14
time_use_thy "Primrec";
paulson@3294
    15
paulson@8944
    16
time_use_thy "NatSum";
clasohm@1351
    17
time_use     "cla.ML";
clasohm@1351
    18
time_use     "meson.ML";
clasohm@1351
    19
time_use     "mesontest.ML";
paulson@8557
    20
time_use     "mesontest2.ML";
lcp@1174
    21
time_use_thy "BT";
nipkow@8797
    22
time_use_thy "AVL";
nipkow@1026
    23
time_use_thy "InSort";
nipkow@1026
    24
time_use_thy "Qsort";
nipkow@1026
    25
time_use_thy "Puzzle";
paulson@3294
    26
paulson@5078
    27
time_use_thy "IntRing";
paulson@5078
    28
wenzelm@9100
    29
time_use_thy "set";
nipkow@1026
    30
time_use_thy "MT";
paulson@7085
    31
time_use_thy "Tarski";
clasohm@1296
    32
wenzelm@5199
    33
time_use_thy "StringEx";
wenzelm@5199
    34
time_use_thy "BinEx";
paulson@7187
    35
wenzelm@7304
    36
if_svc_enabled time_use_thy "svc_test";
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@8569
    48
time_use_thy "Multiquote";