src/HOL/ex/ROOT.ML
author wenzelm
Thu Sep 27 15:42:08 2001 +0200 (2001-09-27)
changeset 11586 d8a7f6318457
parent 11445 01ee48a80800
child 12080 4c1e3a2a87c3
permissions -rw-r--r--
tuned;
wenzelm@9000
     1
(*  Title:      HOL/ex/ROOT.ML
clasohm@969
     2
    ID:         $Id$
clasohm@969
     3
wenzelm@9297
     4
Miscellaneous examples for Higher-Order Logic.
clasohm@969
     5
*)
clasohm@969
     6
wenzelm@5753
     7
(*some examples of recursive function definitions: the TFL package*)
wenzelm@5124
     8
time_use_thy "Recdefs";
paulson@3337
     9
time_use_thy "Primrec";
paulson@3294
    10
wenzelm@11586
    11
setmp proofs 2 time_use_thy "Hilbert_Classical";
wenzelm@11586
    12
wenzelm@11586
    13
(*advanced concrete syntax*)
wenzelm@11586
    14
time_use_thy "Tuple";
wenzelm@11586
    15
time_use_thy "Antiquote";
wenzelm@11586
    16
time_use_thy "Multiquote";
wenzelm@11586
    17
wenzelm@11586
    18
(*basic use of extensible records*)
wenzelm@11586
    19
time_use_thy "MonoidGroup";
wenzelm@11586
    20
time_use_thy "Records";
wenzelm@11586
    21
wenzelm@11586
    22
time_use_thy "StringEx";
wenzelm@11586
    23
time_use_thy "BinEx";
wenzelm@11586
    24
paulson@8944
    25
time_use_thy "NatSum";
clasohm@1351
    26
time_use     "cla.ML";
clasohm@1351
    27
time_use     "mesontest.ML";
wenzelm@10440
    28
time_use_thy "mesontest2";
lcp@1174
    29
time_use_thy "BT";
nipkow@8797
    30
time_use_thy "AVL";
nipkow@1026
    31
time_use_thy "InSort";
nipkow@1026
    32
time_use_thy "Qsort";
nipkow@1026
    33
time_use_thy "Puzzle";
paulson@3294
    34
paulson@5078
    35
time_use_thy "IntRing";
paulson@5078
    36
wenzelm@9100
    37
time_use_thy "set";
nipkow@1026
    38
time_use_thy "MT";
paulson@7085
    39
time_use_thy "Tarski";
clasohm@1296
    40
wenzelm@7304
    41
if_svc_enabled time_use_thy "svc_test";