src/HOL/IMP/ROOT.ML
author wenzelm
Fri Dec 19 10:28:33 1997 +0100 (1997-12-19)
changeset 4449 df30e75f670f
parent 1696 e84bff5c519b
child 6349 f7750d816c21
permissions -rw-r--r--
tuned;
clasohm@1465
     1
(*  Title:      HOL/IMP/ROOT.ML
clasohm@924
     2
    ID:         $Id$
clasohm@1465
     3
    Author:     Heiko Loetzbeyer, Robert Sandner, Tobias Nipkow
nipkow@936
     4
    Copyright   1995 TUM
clasohm@924
     5
*)
clasohm@924
     6
clasohm@1465
     7
HOL_build_completed;    (*Make examples fail if HOL did*)
clasohm@924
     8
clasohm@1165
     9
writeln"Root file for HOL/IMP";
wenzelm@4449
    10
set proof_timing;
nipkow@1696
    11
time_use_thy "Expr";
nipkow@1696
    12
time_use_thy "Transition";
nipkow@1447
    13
time_use_thy "VC";