src/HOL/W0/ROOT.ML
changeset 12944 fa6a3ddec27f
parent 9000 c20d58286a51
child 33615 261abc2e3155
     1.1 --- a/src/HOL/W0/ROOT.ML	Mon Feb 25 20:51:48 2002 +0100
     1.2 +++ b/src/HOL/W0/ROOT.ML	Tue Feb 26 00:19:04 2002 +0100
     1.3 @@ -1,13 +1,2 @@
     1.4 -(*  Title:      HOL/W0/ROOT.ML
     1.5 -    ID:         $Id$
     1.6 -    Author:     Tobias Nipkow
     1.7 -    Copyright   1995 TUM
     1.8  
     1.9 -Type inference for let-free MiniML
    1.10 -*)
    1.11 -
    1.12 -Unify.trace_bound := 20;
    1.13 -
    1.14 -AddSEs [less_SucE];
    1.15 -
    1.16 -time_use_thy "I";
    1.17 +use_thy "W0";