diff -r eacce1cd716a -r 05fc32a23b8b doc-src/TutorialI/Misc/document/prime_def.tex --- a/doc-src/TutorialI/Misc/document/prime_def.tex Tue Aug 16 13:42:21 2005 +0200 +++ b/doc-src/TutorialI/Misc/document/prime_def.tex Tue Aug 16 13:42:23 2005 +0200 @@ -1,8 +1,20 @@ % \begin{isabellebody}% \def\isabellecontext{prime{\isacharunderscore}def}% -\isamarkupfalse% -\isamarkupfalse% +% +\isadelimtheory +% +\endisadelimtheory +% +\isatagtheory +% +\endisatagtheory +{\isafoldtheory}% +% +\isadelimtheory +% +\endisadelimtheory +\isamarkuptrue% % \begin{isamarkuptext}% \begin{warn} @@ -21,8 +33,19 @@ \end{isabelle} \end{warn}% \end{isamarkuptext}% -\isamarkuptrue% -\isamarkupfalse% +% +\isadelimtheory +% +\endisadelimtheory +% +\isatagtheory +% +\endisatagtheory +{\isafoldtheory}% +% +\isadelimtheory +% +\endisadelimtheory \end{isabellebody}% %%% Local Variables: %%% mode: latex