| changeset 10267 | 325ead6d9457 |
| parent 10187 | 0376cccd9118 |
| child 11456 | 7eb63f63e6c6 |
--- a/doc-src/TutorialI/Misc/document/prime_def.tex Wed Oct 18 23:44:52 2000 +0200 +++ b/doc-src/TutorialI/Misc/document/prime_def.tex Wed Oct 18 23:58:07 2000 +0200 @@ -1,6 +1,6 @@ % \begin{isabellebody}% -\def\isabellecontext{prime_def}% +\def\isabellecontext{prime{\isacharunderscore}def}% % \begin{isamarkuptext}% \begin{warn}