src/HOL/ex/ROOT.ML
author nipkow
Fri May 05 12:51:33 2000 +0200 (2000-05-05)
changeset 8797 b55e2354d71e
parent 8569 748a9699f28d
child 8933 de96f2982d2c
permissions -rw-r--r--
Added AVL
     1 (*  Title:      HOL/ex/ROOT
     2     ID:         $Id$
     3     Author:     Tobias Nipkow, Cambridge University Computer Laboratory
     4     Copyright   1991  University of Cambridge
     5 
     6 Executes miscellaneous examples for Higher-Order Logic. 
     7 *)
     8 
     9 writeln "Root file for HOL examples";
    10 
    11 set proof_timing;
    12 
    13 (*some examples of recursive function definitions: the TFL package*)
    14 time_use_thy "Recdefs";
    15 time_use_thy "Primes";
    16 time_use_thy "Fib";
    17 with_path "../Induct" use_thy "Factorization";
    18 time_use_thy "Primrec";
    19 
    20 time_use_thy "NatSum";
    21 time_use     "cla.ML";
    22 time_use     "meson.ML";
    23 time_use     "mesontest.ML";
    24 time_use     "mesontest2.ML";
    25 time_use_thy "BT";
    26 time_use_thy "AVL";
    27 time_use_thy "InSort";
    28 time_use_thy "Qsort";
    29 time_use_thy "Puzzle";
    30 
    31 time_use_thy "IntRing";
    32 
    33 time_use     "set.ML";
    34 time_use_thy "MT";
    35 time_use_thy "Tarski";
    36 
    37 time_use_thy "StringEx";
    38 time_use_thy "BinEx";
    39 
    40 if_svc_enabled time_use_thy "svc_test";
    41 
    42 (*basic use of extensible records*)
    43 time_use_thy "MonoidGroup";
    44 time_use_thy "Points";
    45 
    46 (*groups via locales*)
    47 time_use_thy "PiSets";
    48 time_use_thy "LocaleGroup";
    49 
    50 (*expressions with quote / antiquote syntax*)
    51 time_use_thy "Antiquote";
    52 time_use_thy "Multiquote";
    53 
    54 
    55 writeln "END: Root file for HOL examples";