# HG changeset patch
# User wenzelm
# Date 1163601562 -3600
# Node ID 18efe191bd5f86a59c4284323a5b74ef6c19a599
# Parent  ae8a112b62d71b3545e993156e6f475ab99d2ca2
updated;

diff -r ae8a112b62d7 -r 18efe191bd5f doc-src/IsarImplementation/Thy/document/base.tex
--- a/doc-src/IsarImplementation/Thy/document/base.tex	Wed Nov 15 15:37:34 2006 +0100
+++ b/doc-src/IsarImplementation/Thy/document/base.tex	Wed Nov 15 15:39:22 2006 +0100
@@ -13,7 +13,7 @@
 \isacommand{theory}\isamarkupfalse%
 \ base\isanewline
 \isakeyword{imports}\ CPure\isanewline
-\isakeyword{uses}\ {\isachardoublequoteopen}setup{\isachardot}ML{\isachardoublequoteclose}\isanewline
+\isakeyword{uses}\ {\isachardoublequoteopen}{\isachardot}{\isachardot}{\isacharslash}{\isachardot}{\isachardot}{\isacharslash}antiquote{\isacharunderscore}setup{\isachardot}ML{\isachardoublequoteclose}\isanewline
 \isakeyword{begin}\isanewline
 \isanewline
 \isacommand{end}\isamarkupfalse%