diff -r ebe2253e5c0e -r 93e7935d4cb5 doc-src/IsarImplementation/Thy/document/Base.tex
--- a/doc-src/IsarImplementation/Thy/document/Base.tex	Mon Oct 25 11:01:00 2010 +0200
+++ b/doc-src/IsarImplementation/Thy/document/Base.tex	Mon Oct 25 11:16:23 2010 +0200
@@ -11,41 +11,8 @@
 \ Base\isanewline
 \isakeyword{imports}\ Main\isanewline
 \isakeyword{uses}\ {\isachardoublequoteopen}{\isachardot}{\isachardot}{\isacharslash}{\isachardot}{\isachardot}{\isacharslash}antiquote{\isacharunderscore}setup{\isachardot}ML{\isachardoublequoteclose}\isanewline
-\isakeyword{begin}%
-\endisatagtheory
-{\isafoldtheory}%
-%
-\isadelimtheory
-\isanewline
-%
-\endisadelimtheory
-\isanewline
-%
-\isadelimML
+\isakeyword{begin}\isanewline
 \isanewline
-%
-\endisadelimML
-%
-\isatagML
-\isacommand{ML}\isamarkupfalse%
-\ {\isacharverbatimopen}\isanewline
-\ \ ML{\isacharunderscore}Antiquote{\isachardot}inline\ {\isachardoublequote}assert{\isachardoublequote}\isanewline
-\ \ \ \ {\isacharparenleft}Scan{\isachardot}succeed\ {\isachardoublequote}{\isacharparenleft}fn\ b\ {\isacharequal}{\isachargreater}\ if\ b\ then\ {\isacharparenleft}{\isacharparenright}\ else\ raise\ General{\isachardot}Fail\ {\isacharbackslash}{\isachardoublequote}Assertion\ failed{\isacharbackslash}{\isachardoublequote}{\isacharparenright}{\isachardoublequote}{\isacharparenright}\isanewline
-{\isacharverbatimclose}%
-\endisatagML
-{\isafoldML}%
-%
-\isadelimML
-\isanewline
-%
-\endisadelimML
-%
-\isadelimtheory
-\isanewline
-%
-\endisadelimtheory
-%
-\isatagtheory
 \isacommand{end}\isamarkupfalse%
 %
 \endisatagtheory