# HG changeset patch
# User wenzelm
# Date 967650912 -7200
# Node ID a09f4a7acceab2e2d42dda25680e27430725c193
# Parent  1287787744a79b06eeef4aad6c4f37e9fee21822
renamed antiquotation 'name' to 'text';
added antiquotation option 'source';

diff -r 1287787744a7 -r a09f4a7accea doc-src/IsarRef/syntax.tex
--- a/doc-src/IsarRef/syntax.tex	Wed Aug 30 17:54:46 2000 +0200
+++ b/doc-src/IsarRef/syntax.tex	Wed Aug 30 17:55:12 2000 +0200
@@ -348,9 +348,9 @@
 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 \texttt{name}
-antiquotation is an exception to this rule: it prints an uninterpreted text
-argument that is not checked in any way.
+the current theory or proof context can be ensured.  The $text$ 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{name}
@@ -363,7 +363,7 @@
     'prop' options prop |
     'term' options term |
     'typ' options type |
-    'name' options name
+    'text' options name
   ;
   options: '[' (option * ',') ']'
   ;
@@ -395,6 +395,10 @@
   ``$xsymbols$'', ``$symbols$''.
 \item[$margin = nat$ and $indent = nat$] change the margin or indentation for
   pretty printing of display material.
+\item[$source = bool$] prints the source text of the antiquotation arguments,
+  rather than the actual value.  Note that this does not affect
+  well-formedness checks of $thm$, $term$, etc. (only the $text$ antiquotation
+  admits arbitrary output).
 \end{descr}
 
 For boolean flags, ``$name = true$'' may be abbreviated as ``$name$''.  All of