src/HOL/ex/ROOT.ML
changeset 10052 5fa8d8d5c852
parent 9942 87f0809a06a9
child 10440 2074e62da354
     1.1 --- a/src/HOL/ex/ROOT.ML	Thu Sep 21 14:55:46 2000 +0200
     1.2 +++ b/src/HOL/ex/ROOT.ML	Thu Sep 21 15:58:13 2000 +0200
     1.3 @@ -31,7 +31,7 @@
     1.4  
     1.5  (*basic use of extensible records*)
     1.6  time_use_thy "MonoidGroup";
     1.7 -time_use_thy "Points";
     1.8 +time_use_thy "Records";
     1.9  
    1.10  (*groups via locales*)
    1.11  time_use_thy "PiSets";