# HG changeset patch
# User wenzelm
# Date 1218740767 -7200
# Node ID f0d543629376cc025d3143069442f08cc29de8ed
# Parent  4ab10bfe8a7f65fb8b4977f28b109fc9fff63a6a
[source=false] for quoted antiquotation avoids quote-escapes in output;

diff -r 4ab10bfe8a7f -r f0d543629376 doc-src/IsarRef/Thy/Document_Preparation.thy
--- a/doc-src/IsarRef/Thy/Document_Preparation.thy	Thu Aug 14 20:29:38 2008 +0200
+++ b/doc-src/IsarRef/Thy/Document_Preparation.thy	Thu Aug 14 21:06:07 2008 +0200
@@ -159,7 +159,7 @@
   terms and types, which are to be presented in the final output
   produced by the Isabelle document preparation system.
 
-  Thus embedding of ``@{text "@{term [show_types] \"f x = a + x\"}"}''
+  Thus embedding of ``@{text [source=false] "@{term [show_types] \"f x = a + x\"}"}''
   within a text block would cause
   \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
   antiquotations may involve attributes as well.  For example,
diff -r 4ab10bfe8a7f -r f0d543629376 doc-src/IsarRef/Thy/document/Document_Preparation.tex
--- a/doc-src/IsarRef/Thy/document/Document_Preparation.tex	Thu Aug 14 20:29:38 2008 +0200
+++ b/doc-src/IsarRef/Thy/document/Document_Preparation.tex	Thu Aug 14 21:06:07 2008 +0200
@@ -175,7 +175,7 @@
   terms and types, which are to be presented in the final output
   produced by the Isabelle document preparation system.
 
-  Thus embedding of ``\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}term\ {\isacharbrackleft}show{\isacharunderscore}types{\isacharbrackright}\ {\isachardoublequote}f\ x\ {\isacharequal}\ a\ {\isacharplus}\ x{\isachardoublequote}{\isacharbraceright}{\isachardoublequote}}''
+  Thus embedding of ``\isa{{\isacharat}{\isacharbraceleft}term\ {\isacharbrackleft}show{\isacharunderscore}types{\isacharbrackright}\ {\isachardoublequote}f\ x\ {\isacharequal}\ a\ {\isacharplus}\ x{\isachardoublequote}{\isacharbraceright}}''
   within a text block would cause
   \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
   antiquotations may involve attributes as well.  For example,