doc-src/System/Thy/document/Presentation.tex

 
   \medskip The \verb|-t| option tells {\LaTeX} how to interpret
   tagged Isabelle command regions.  Tags are specified as a comma
   separated list of modifier/name pairs: ``\verb|+|\isa{foo}'' (or just ``\isa{foo}'') means to keep, ``\verb|-|\isa{foo}'' to drop, and ``\verb|/|\isa{foo}'' to
   fold text tagged as \isa{foo}.  The builtin default is equivalent
-  to the tag specification ``\verb|/theory,/proof,/ML,+visible,-invisible|''; see also the {\LaTeX}
+  to the tag specification ``\verb|+theory,+proof,+ML,+visible,-invisible|''; see also the {\LaTeX}
   macros \verb|\isakeeptag|, \verb|\isadroptag|, and
   \verb|\isafoldtag|, in \hyperlink{file.~~/lib/texinputs/isabelle.sty}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}lib{\isacharslash}texinputs{\isacharslash}isabelle{\isachardot}sty}}}}.
 
   \medskip Document preparation requires a properly setup ``\verb|document|'' directory within the logic session sources.  This
   directory is supposed to contain all the files needed to produce the