diff -r 725a91601ed1 -r 27ea2ba48fa3 doc-src/IsarImplementation/Thy/locale.thy
--- a/doc-src/IsarImplementation/Thy/locale.thy	Thu Aug 31 18:27:40 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/locale.thy	Thu Aug 31 22:55:49 2006 +0200
@@ -9,8 +9,18 @@
 
 text FIXME
 
-section {* Locales *}
+
+section {* Type-checking specifications *}
 
 text FIXME
 
+
+section {* Localized theory specifications *}
+
+text {*
+  FIXME
+
+  \glossary{Local theory}{FIXME}
+*}
+
 end