doc-src/IsarRef/Thy/document/HOL_Specific.tex
changeset 43501 a55e0663ad1d
parent 43498 8749742785b8
child 43522 e3fdb7c96be5
     1.1 --- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Mon May 02 21:42:36 2011 +0200
     1.2 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Mon May 02 21:46:54 2011 +0200
     1.3 @@ -10,7 +10,6 @@
     1.4  \isacommand{theory}\isamarkupfalse%
     1.5  \ HOL{\isaliteral{5F}{\isacharunderscore}}Specific\isanewline
     1.6  \isakeyword{imports}\ Main\isanewline
     1.7 -\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
     1.8  \isakeyword{begin}%
     1.9  \endisatagtheory
    1.10  {\isafoldtheory}%