src/HOL/ex/ROOT.ML
author nipkow
Thu Apr 15 14:17:45 2004 +0200 (2004-04-15)
changeset 14569 78b75a9eec01
parent 14494 48ae8d678d88
child 14592 dd1a2905ea73
permissions -rw-r--r--
Added ex/Exceptions.thy
wenzelm@12115
     1
(*  Title:      HOL/ex/ROOT.ML
wenzelm@12115
     2
    ID:         $Id$
wenzelm@11586
     3
wenzelm@12115
     4
Miscellaneous examples for Higher-Order Logic.
wenzelm@12115
     5
*)
wenzelm@12115
     6
wenzelm@12360
     7
time_use_thy "Higher_Order_Logic";
wenzelm@12360
     8
wenzelm@12115
     9
time_use_thy "Recdefs";
paulson@14244
    10
time_use_thy "InductiveInvariant_examples";
wenzelm@12115
    11
time_use_thy "Primrec";
wenzelm@12276
    12
time_use_thy "Locales";
wenzelm@12115
    13
time_use_thy "Records";
wenzelm@12115
    14
time_use_thy "MonoidGroup";
wenzelm@12115
    15
time_use_thy "StringEx";
wenzelm@12115
    16
time_use_thy "BinEx";
wenzelm@12115
    17
setmp proofs 2 time_use_thy "Hilbert_Classical";
wenzelm@12115
    18
time_use_thy "Antiquote";
wenzelm@12115
    19
time_use_thy "Multiquote";
wenzelm@12115
    20
time_use_thy "Tuple";
wenzelm@12115
    21
wenzelm@12115
    22
time_use_thy "NatSum";
berghofe@12450
    23
time_use_thy "Intuitionistic";
paulson@14220
    24
time_use_thy "Classical";
wenzelm@12115
    25
time_use_thy "mesontest2";
berghofe@13880
    26
time_use_thy "PresburgerEx";
wenzelm@12115
    27
time_use_thy "BT";
wenzelm@12115
    28
time_use_thy "InSort";
wenzelm@12115
    29
time_use_thy "Qsort";
nipkow@13200
    30
time_use_thy "MergeSort";
wenzelm@12115
    31
time_use_thy "Puzzle";
wenzelm@12115
    32
nipkow@14569
    33
no_document use_thy "List_Prefix";
nipkow@14569
    34
time_use_thy "Exceptions";
nipkow@14569
    35
wenzelm@12115
    36
time_use_thy "IntRing";
wenzelm@12115
    37
wenzelm@12115
    38
time_use_thy "set";
wenzelm@12115
    39
time_use_thy "MT";
nipkow@14569
    40
nipkow@14569
    41
no_document use_thy "FuncSet";
wenzelm@12115
    42
time_use_thy "Tarski";
wenzelm@12115
    43
wenzelm@12869
    44
time_use_thy "SVC_Oracle";
wenzelm@12115
    45
if_svc_enabled time_use_thy "svc_test";
webertj@14459
    46
webertj@14462
    47
time_use_thy "Refute_Examples";
skalberg@14494
    48
nipkow@14569
    49
no_document use_thy "Word";
skalberg@14494
    50
time_use_thy "Adder";
nipkow@14569
    51