# HG changeset patch
# User wenzelm
# Date 967572755 -7200
# Node ID 1546ad1c78396b60fe875a580dd71d810b7abad0
# Parent  5e18de753e0f52140e1f3dd992f603603828a5d3
added antiquotation 'name' and option 'indent';

diff -r 5e18de753e0f -r 1546ad1c7839 doc-src/IsarRef/syntax.tex
--- a/doc-src/IsarRef/syntax.tex	Tue Aug 29 20:12:04 2000 +0200
+++ b/doc-src/IsarRef/syntax.tex	Tue Aug 29 20:12:35 2000 +0200
@@ -345,14 +345,15 @@
 \isa{(f{\isasymColon}'a~{\isasymRightarrow}~'a)~(x{\isasymColon}'a)~=~(a{\isasymColon}'a)~+~x}
 to appear in the final {\LaTeX} document.
 
-\medskip
-
 Antiquotations do not only spare the author from tedious typing, but also
 achieve some degree of consistency-checking of informal explanations with
 formal developments, since well-formedness of terms and types with respect to
-the current theory or proof context can be ensured.
+the current theory or proof context can be ensured.  The \texttt{name}
+antiquotation is an exception to this rule: it prints an uninterpreted text
+argument that is not checked in any way.
 
-\indexisarant{thm}\indexisarant{prop}\indexisarant{term}\indexisarant{typ}
+\indexisarant{thm}\indexisarant{prop}\indexisarant{term}
+\indexisarant{typ}\indexisarant{name}
 \begin{rail}
   atsign lbrace antiquotation rbrace
   ;
@@ -361,7 +362,8 @@
     'thm' options thmrefs |
     'prop' options prop |
     'term' options term |
-    'typ' options type
+    'typ' options type |
+    'name' options name
   ;
   options: '[' (option * ',') ']'
   ;
@@ -391,8 +393,8 @@
   (see also \cite{isabelle-ref}).  Note that the standard setup for {\LaTeX}
   output is already present by default, including the modes ``$latex$'',
   ``$xsymbols$'', ``$symbols$''.
-\item[$margin = nat$] changes the margin for pretty printing of display
-  material.
+\item[$margin = nat$ and $indent = nat$] change the margin or indentation for
+  pretty printing of display material.
 \end{descr}
 
 For boolean flags, ``$name = true$'' may be abbreviated as ``$name$''.  All of