diff -r aeabb735883a -r 9864182c6bad doc-src/IsarImplementation/Thy/document/Base.tex --- a/doc-src/IsarImplementation/Thy/document/Base.tex Mon Jun 27 17:51:28 2011 +0200 +++ b/doc-src/IsarImplementation/Thy/document/Base.tex Mon Jun 27 22:20:49 2011 +0200 @@ -11,8 +11,37 @@ \ Base\isanewline \isakeyword{imports}\ Main\isanewline \isakeyword{uses}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2F}{\isacharslash}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2F}{\isacharslash}}antiquote{\isaliteral{5F}{\isacharunderscore}}setup{\isaliteral{2E}{\isachardot}}ML{\isaliteral{22}{\isachardoublequoteclose}}\isanewline -\isakeyword{begin}\isanewline +\isakeyword{begin}% +\endisatagtheory +{\isafoldtheory}% +% +\isadelimtheory +\isanewline +% +\endisadelimtheory +% +\isadelimML \isanewline +% +\endisadelimML +% +\isatagML +\isacommand{setup}\isamarkupfalse% +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\ Antiquote{\isaliteral{5F}{\isacharunderscore}}Setup{\isaliteral{2E}{\isachardot}}setup\ {\isaliteral{2A7D}{\isacharverbatimclose}}% +\endisatagML +{\isafoldML}% +% +\isadelimML +\isanewline +% +\endisadelimML +% +\isadelimtheory +\isanewline +% +\endisadelimtheory +% +\isatagtheory \isacommand{end}\isamarkupfalse% % \endisatagtheory