--- 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