src/HOL/ex/ROOT.ML
author clasohm
Wed Mar 22 12:42:34 1995 +0100 (1995-03-22)
changeset 969 b051e2fc2e34
child 970 6d36fe1bb234
permissions -rw-r--r--
converted ex with curried function application
clasohm@969
     1
(*  Title:  	HOL/ex/ROOT
clasohm@969
     2
    ID:         $Id$
clasohm@969
     3
    Author: 	Tobias Nipkow, Cambridge University Computer Laboratory
clasohm@969
     4
    Copyright   1991  University of Cambridge
clasohm@969
     5
clasohm@969
     6
Executes miscellaneous examples for Higher-Order Logic. 
clasohm@969
     7
*)
clasohm@969
     8
clasohm@969
     9
HOL_build_completed;    (*Cause examples to fail if HOL did*)
clasohm@969
    10
clasohm@969
    11
(writeln"Root file for HOL examples";
clasohm@969
    12
 proof_timing := true;
clasohm@969
    13
 loadpath := ["ex"];
clasohm@969
    14
 time_use     "ex/cla.ML";
clasohm@969
    15
 time_use     "ex/meson.ML";
clasohm@969
    16
 time_use     "ex/mesontest.ML";
clasohm@969
    17
 time_use_thy "String";
clasohm@969
    18
 time_use_thy "InSort";
clasohm@969
    19
 time_use_thy "Qsort";
clasohm@969
    20
 time_use_thy "LexProd";
clasohm@969
    21
 time_use_thy "Puzzle";
clasohm@969
    22
 time_use_thy "NatSum";
clasohm@969
    23
 time_use     "ex/set.ML";
clasohm@969
    24
 time_use_thy "SList";
clasohm@969
    25
 time_use_thy "LList";
clasohm@969
    26
 time_use_thy "Acc";
clasohm@969
    27
 time_use_thy "PropLog";
clasohm@969
    28
 time_use_thy "Term";
clasohm@969
    29
 time_use_thy "Simult";
clasohm@969
    30
 time_use_thy "MT";
clasohm@969
    31
 writeln     "END: Root file for HOL examples"
clasohm@969
    32
)  handle _ => exit 1;