doc-src/IsarRef/Thy/document/Document_Preparation.tex
changeset 27881 f0d543629376
parent 27453 eecd9d84e41b
child 28505 f98751bd715f
     1.1 --- a/doc-src/IsarRef/Thy/document/Document_Preparation.tex	Thu Aug 14 20:29:38 2008 +0200
     1.2 +++ b/doc-src/IsarRef/Thy/document/Document_Preparation.tex	Thu Aug 14 21:06:07 2008 +0200
     1.3 @@ -175,7 +175,7 @@
     1.4    terms and types, which are to be presented in the final output
     1.5    produced by the Isabelle document preparation system.
     1.6  
     1.7 -  Thus embedding of ``\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}term\ {\isacharbrackleft}show{\isacharunderscore}types{\isacharbrackright}\ {\isachardoublequote}f\ x\ {\isacharequal}\ a\ {\isacharplus}\ x{\isachardoublequote}{\isacharbraceright}{\isachardoublequote}}''
     1.8 +  Thus embedding of ``\isa{{\isacharat}{\isacharbraceleft}term\ {\isacharbrackleft}show{\isacharunderscore}types{\isacharbrackright}\ {\isachardoublequote}f\ x\ {\isacharequal}\ a\ {\isacharplus}\ x{\isachardoublequote}{\isacharbraceright}}''
     1.9    within a text block would cause
    1.10    \isa{{\isacharparenleft}f{\isasymColon}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isacharparenright}\ {\isacharparenleft}x{\isasymColon}{\isacharprime}a{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}a{\isasymColon}{\isacharprime}a{\isacharparenright}\ {\isacharplus}\ x} to appear in the final {\LaTeX} document.  Also note that theorem
    1.11    antiquotations may involve attributes as well.  For example,