time_use_thy "Locales";
authorwenzelm
Fri Nov 23 19:19:35 2001 +0100 (2001-11-23)
changeset 122767bafe3d6c248
parent 12275 aa2b7b475a94
child 12277 2b28d7dd91f5
time_use_thy "Locales";
src/HOL/ex/ROOT.ML
     1.1 --- a/src/HOL/ex/ROOT.ML	Fri Nov 23 17:19:14 2001 +0100
     1.2 +++ b/src/HOL/ex/ROOT.ML	Fri Nov 23 19:19:35 2001 +0100
     1.3 @@ -6,7 +6,7 @@
     1.4  
     1.5  time_use_thy "Recdefs";
     1.6  time_use_thy "Primrec";
     1.7 -(* FIXME time_use_thy "Locales"; *)
     1.8 +time_use_thy "Locales";
     1.9  time_use_thy "Records";
    1.10  time_use_thy "MonoidGroup";
    1.11  time_use_thy "StringEx";