1.1 --- a/doc-src/IsarRef/Thy/Document_Preparation.thy	Thu Aug 14 20:29:38 2008 +0200
     1.2 +++ b/doc-src/IsarRef/Thy/Document_Preparation.thy	Thu Aug 14 21:06:07 2008 +0200
     1.3 @@ -159,7 +159,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 ``@{text "@{term [show_types] \"f x = a + x\"}"}''
     1.8 +  Thus embedding of ``@{text [source=false] "@{term [show_types] \"f x = a + x\"}"}''
     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,

     2.1 --- a/doc-src/IsarRef/Thy/document/Document_Preparation.tex	Thu Aug 14 20:29:38 2008 +0200
     2.2 +++ b/doc-src/IsarRef/Thy/document/Document_Preparation.tex	Thu Aug 14 21:06:07 2008 +0200
     2.3 @@ -175,7 +175,7 @@
     2.4    terms and types, which are to be presented in the final output
     2.5    produced by the Isabelle document preparation system.
     2.6  
     2.7 -  Thus embedding of ``\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}term\ {\isacharbrackleft}show{\isacharunderscore}types{\isacharbrackright}\ {\isachardoublequote}f\ x\ {\isacharequal}\ a\ {\isacharplus}\ x{\isachardoublequote}{\isacharbraceright}{\isachardoublequote}}''
     2.8 +  Thus embedding of ``\isa{{\isacharat}{\isacharbraceleft}term\ {\isacharbrackleft}show{\isacharunderscore}types{\isacharbrackright}\ {\isachardoublequote}f\ x\ {\isacharequal}\ a\ {\isacharplus}\ x{\isachardoublequote}{\isacharbraceright}}''
     2.9    within a text block would cause
    2.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
    2.11    antiquotations may involve attributes as well.  For example,