doc-src/Classes/Thy/document/Classes.tex
changeset 37216 3165bc303f66
parent 35282 8fd9d555d04d
child 37610 1b09880d9734
--- a/doc-src/Classes/Thy/document/Classes.tex	Mon May 31 19:36:13 2010 +0200
+++ b/doc-src/Classes/Thy/document/Classes.tex	Mon May 31 21:06:57 2010 +0200
@@ -792,8 +792,7 @@
 \isamarkuptrue%
 %
 \begin{isamarkuptext}%
-Isabelle locales support a concept of local definitions
-  in locales:%
+Isabelle locales are targets which support local definitions:%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %