diff -r f61ac1573ee6 -r a55e0663ad1d doc-src/IsarRef/Thy/document/HOL_Specific.tex
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Mon May 02 21:42:36 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Mon May 02 21:46:54 2011 +0200
@@ -10,7 +10,6 @@
 \isacommand{theory}\isamarkupfalse%
 \ HOL{\isaliteral{5F}{\isacharunderscore}}Specific\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}%