src/HOL/Algebra/ROOT.ML
changeset 9000 c20d58286a51
parent 8010 69032a618aa9
child 13870 cf947d1ec5ff
     1.1 --- a/src/HOL/Algebra/ROOT.ML	Tue May 30 16:03:09 2000 +0200
     1.2 +++ b/src/HOL/Algebra/ROOT.ML	Tue May 30 16:08:38 2000 +0200
     1.3 @@ -4,5 +4,5 @@
     1.4      Author: Clemens Ballarin, started 24 September 1999
     1.5  *)
     1.6  
     1.7 -with_path "abstract" use_thy "Abstract";        (*The ring theory*)
     1.8 -with_path "poly"     use_thy "Polynomial";      (*The full theory*)
     1.9 +with_path "abstract" time_use_thy "Abstract";        (*The ring theory*)
    1.10 +with_path "poly"     time_use_thy "Polynomial";      (*The full theory*)