src/CTT/ex/ROOT.ML
author paulson
Tue Apr 30 11:08:09 1996 +0200 (1996-04-30)
changeset 1702 4aa538e82f76
parent 1459 d12da312eff4
child 2822 50bac845de6f
permissions -rw-r--r--
Cosmetic re-ordering of declarations
     1 (*  Title:      CTT/ex/ROOT
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1991  University of Cambridge
     5 
     6 Executes all examples for Constructive Type Theory. 
     7 *)
     8 
     9 CTT_build_completed;    (*Cause examples to fail if CTT did*)
    10 
    11 writeln"Root file for CTT examples";
    12 
    13 print_depth 2;  
    14 proof_timing := true;
    15 time_use "ex/typechk.ML";
    16 time_use "ex/elim.ML";
    17 time_use "ex/equal.ML";
    18 time_use "ex/synth.ML";
    19 
    20 maketest"END: Root file for CTT examples";