doc-src/IsarImplementation/Thy/document/Base.tex

--- a/doc-src/IsarImplementation/Thy/document/Base.tex	Wed Aug 22 23:23:48 2012 +0200
+++ b/doc-src/IsarImplementation/Thy/document/Base.tex	Wed Aug 22 23:45:49 2012 +0200
@@ -10,7 +10,6 @@
 \isacommand{theory}\isamarkupfalse%
 \ 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}%
 \endisatagtheory
 {\isafoldtheory}%
@@ -26,6 +25,8 @@
 \endisadelimML
 %
 \isatagML
+\isacommand{ML{\isaliteral{5F}{\isacharunderscore}}file}\isamarkupfalse%
+\ {\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
 \isacommand{setup}\isamarkupfalse%
 \ {\isaliteral{7B2A}{\isacharverbatimopen}}\ Antiquote{\isaliteral{5F}{\isacharunderscore}}Setup{\isaliteral{2E}{\isachardot}}setup\ {\isaliteral{2A7D}{\isacharverbatimclose}}%
 \endisatagML