--- a/doc-src/IsarRef/syntax.tex Mon Nov 13 18:19:24 2006 +0100
+++ b/doc-src/IsarRef/syntax.tex Mon Nov 13 20:08:20 2006 +0100
@@ -430,6 +430,7 @@
\subsection{Antiquotations}\label{sec:antiq}
\begin{matharray}{rcl}
+ theory & : & \isarantiq \\
thm & : & \isarantiq \\
prop & : & \isarantiq \\
term & : & \isarantiq \\
@@ -463,7 +464,7 @@
statement where all schematic variables have been replaced by fixed ones,
which are easier to read.
-\indexisarant{thm}\indexisarant{prop}\indexisarant{term}\indexisarant{const}
+\indexisarant{theory}\indexisarant{thm}\indexisarant{prop}\indexisarant{term}\indexisarant{const}
\indexisarant{typeof}\indexisarant{typ}\indexisarant{thm-style}
\indexisarant{term-style}\indexisarant{text}\indexisarant{goals}
\indexisarant{subgoals}\indexisarant{prf}\indexisarant{full-prf}\indexisarant{ML}
@@ -474,6 +475,7 @@
;
antiquotation:
+ 'theory' options name |
'thm' options thmrefs |
'prop' options prop |
'term' options term |
@@ -501,6 +503,9 @@
\texttt{(*~\dots~*)} or verbatim text \verb|{*|~\dots~\verb|*}|.
\begin{descr}
+
+\item [$\at\{theory~A\}$] prints the name $A$, which is guaranteed to
+ refer to a valid theory in the current session.
\item [$\at\{thm~\vec a\}$] prints theorems $\vec a$. Note that attribute
specifications may be included as well (see also \S\ref{sec:syn-att}); the