# HG changeset patch # User wenzelm # Date 1006469193 -3600 # Node ID 2582d16acd3df2d8f1e30836cd8bf8c4db39fd73 # Parent 7fb9840d358d44c6779cad49ac73417488a029c9 theory Locales temporarily disabled; diff -r 7fb9840d358d -r 2582d16acd3d src/HOL/ex/ROOT.ML --- a/src/HOL/ex/ROOT.ML Thu Nov 22 23:45:57 2001 +0100 +++ b/src/HOL/ex/ROOT.ML Thu Nov 22 23:46:33 2001 +0100 @@ -6,7 +6,7 @@ time_use_thy "Recdefs"; time_use_thy "Primrec"; -time_use_thy "Locales"; +(* FIXME time_use_thy "Locales"; *) time_use_thy "Records"; time_use_thy "MonoidGroup"; time_use_thy "StringEx";