# HG changeset patch
# User wenzelm
# Date 1005087076 -3600
# Node ID 4c1e3a2a87c3ef4f6d4c8b74cc4b4eac59643c27
# Parent  054153c48bdeb52f15731658165d96a26d62e090
use_thy "Locales";

diff -r 054153c48bde -r 4c1e3a2a87c3 src/HOL/ex/ROOT.ML
--- a/src/HOL/ex/ROOT.ML	Tue Nov 06 23:51:00 2001 +0100
+++ b/src/HOL/ex/ROOT.ML	Tue Nov 06 23:51:16 2001 +0100
@@ -19,6 +19,7 @@
 time_use_thy "MonoidGroup";
 time_use_thy "Records";
 
+time_use_thy "Locales";
 time_use_thy "StringEx";
 time_use_thy "BinEx";