src/HOL/ex/ROOT.ML
author wenzelm
Thu Nov 22 23:46:33 2001 +0100 (2001-11-22)
changeset 12274 2582d16acd3d
parent 12115 d0d41884f787
child 12276 7bafe3d6c248
permissions -rw-r--r--
theory Locales temporarily disabled;
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@12115
     7
time_use_thy "Recdefs";
wenzelm@12115
     8
time_use_thy "Primrec";
wenzelm@12274
     9
(* FIXME time_use_thy "Locales"; *)
wenzelm@12115
    10
time_use_thy "Records";
wenzelm@12115
    11
time_use_thy "MonoidGroup";
wenzelm@12115
    12
time_use_thy "StringEx";
wenzelm@12115
    13
time_use_thy "BinEx";
wenzelm@12115
    14
setmp proofs 2 time_use_thy "Hilbert_Classical";
wenzelm@12115
    15
time_use_thy "Antiquote";
wenzelm@12115
    16
time_use_thy "Multiquote";
wenzelm@12115
    17
time_use_thy "Tuple";
wenzelm@12115
    18
wenzelm@12115
    19
time_use_thy "NatSum";
wenzelm@12115
    20
time_use     "cla.ML";
wenzelm@12115
    21
time_use     "mesontest.ML";
wenzelm@12115
    22
time_use_thy "mesontest2";
wenzelm@12115
    23
time_use_thy "BT";
wenzelm@12115
    24
time_use_thy "AVL";
wenzelm@12115
    25
time_use_thy "InSort";
wenzelm@12115
    26
time_use_thy "Qsort";
wenzelm@12115
    27
time_use_thy "Puzzle";
wenzelm@12115
    28
wenzelm@12115
    29
time_use_thy "IntRing";
wenzelm@12115
    30
wenzelm@12115
    31
time_use_thy "set";
wenzelm@12115
    32
time_use_thy "MT";
wenzelm@12115
    33
time_use_thy "Tarski";
wenzelm@12115
    34
wenzelm@12115
    35
if_svc_enabled time_use_thy "svc_test";