src/HOL/ex/ROOT.ML
changeset 14603 985eb6708207
parent 14592 dd1a2905ea73
child 15037 19b3b0382303
     1.1 --- a/src/HOL/ex/ROOT.ML	Fri Apr 16 19:04:17 2004 +0200
     1.2 +++ b/src/HOL/ex/ROOT.ML	Fri Apr 16 20:33:16 2004 +0200
     1.3 @@ -33,7 +33,7 @@
     1.4  no_document use_thy "List_Prefix";
     1.5  time_use_thy "Exceptions";
     1.6  
     1.7 -time_use_thy "IntRing";
     1.8 +time_use_thy "Lagrange";
     1.9  
    1.10  time_use_thy "set";
    1.11  time_use_thy "MT";