src/HOL/Quot/ROOT.ML
changeset 9000 c20d58286a51
parent 6349 f7750d816c21
     1.1 --- a/src/HOL/Quot/ROOT.ML	Tue May 30 16:03:09 2000 +0200
     1.2 +++ b/src/HOL/Quot/ROOT.ML	Tue May 30 16:08:38 2000 +0200
     1.3 @@ -1,11 +1,7 @@
     1.4  (*  Title:      HOL/Quot/ROOT.ML
     1.5      ID:         $Id$
     1.6 -    Author:     
     1.7 -    Copyright   
     1.8  
     1.9  Higher-order quotients.
    1.10  *)
    1.11  
    1.12 -writeln"Root file for HOL/Quot";
    1.13 -
    1.14 -use_thy "FRACT";
    1.15 +time_use_thy "FRACT";