src/ZF/IMP/ROOT.ML
changeset 33615 261abc2e3155
parent 9000 c20d58286a51
     1.1 --- a/src/ZF/IMP/ROOT.ML	Wed Nov 11 09:02:37 2009 +0100
     1.2 +++ b/src/ZF/IMP/ROOT.ML	Wed Nov 11 14:15:11 2009 +0100
     1.3 @@ -1,5 +1,4 @@
     1.4  (*  Title:      ZF/IMP/ROOT.ML
     1.5 -    ID:         $Id$
     1.6      Author:     Heiko Loetzbeyer & Robert Sandner, TUM
     1.7      Copyright   1994 TUM
     1.8  
     1.9 @@ -12,4 +11,4 @@
    1.10  
    1.11  *)
    1.12  
    1.13 -time_use_thy "Equiv";
    1.14 +use_thys ["Equiv"];