| changeset 20491 | 98ba42f19995 |
| parent 20490 | e502690952be |
| child 20520 | 05fd007bdeb9 |
--- a/doc-src/IsarImplementation/Thy/document/ML.tex Thu Sep 07 15:16:51 2006 +0200 +++ b/doc-src/IsarImplementation/Thy/document/ML.tex Thu Sep 07 20:12:08 2006 +0200 @@ -43,7 +43,7 @@ } \isamarkuptrue% % -\isamarkupsection{Defining a method that depends on declarations in the context% +\isamarkupsection{A method that depends on declarations in the context% } \isamarkuptrue% %