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% %