src/HOL/ex/ROOT.ML
author wenzelm
Fri Nov 10 19:08:30 2000 +0100 (2000-11-10)
changeset 10440 2074e62da354
parent 10052 5fa8d8d5c852
child 11445 01ee48a80800
permissions -rw-r--r--
proper theory context for mesontest2;
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
paulson@8944
    11
time_use_thy "NatSum";
clasohm@1351
    12
time_use     "cla.ML";
clasohm@1351
    13
time_use     "mesontest.ML";
wenzelm@10440
    14
time_use_thy "mesontest2";
lcp@1174
    15
time_use_thy "BT";
nipkow@8797
    16
time_use_thy "AVL";
nipkow@1026
    17
time_use_thy "InSort";
nipkow@1026
    18
time_use_thy "Qsort";
nipkow@1026
    19
time_use_thy "Puzzle";
paulson@3294
    20
paulson@5078
    21
time_use_thy "IntRing";
paulson@5078
    22
wenzelm@9100
    23
time_use_thy "set";
nipkow@1026
    24
time_use_thy "MT";
paulson@7085
    25
time_use_thy "Tarski";
clasohm@1296
    26
wenzelm@5199
    27
time_use_thy "StringEx";
wenzelm@5199
    28
time_use_thy "BinEx";
paulson@7187
    29
wenzelm@7304
    30
if_svc_enabled time_use_thy "svc_test";
wenzelm@5199
    31
wenzelm@5753
    32
(*basic use of extensible records*)
wenzelm@5199
    33
time_use_thy "MonoidGroup";
wenzelm@10052
    34
time_use_thy "Records";
wenzelm@5199
    35
wenzelm@5753
    36
(*groups via locales*)
wenzelm@5250
    37
time_use_thy "PiSets";
wenzelm@5250
    38
time_use_thy "LocaleGroup";
wenzelm@5250
    39
wenzelm@9354
    40
(*advanced concrete syntax*)
wenzelm@9354
    41
time_use_thy "Tuple";
wenzelm@5368
    42
time_use_thy "Antiquote";
wenzelm@8569
    43
time_use_thy "Multiquote";