# HG changeset patch
# User wenzelm
# Date 1163444900 -3600
# Node ID 320e136db6dc14b88ee0497e3c460ce406c4f126
# Parent  223a3de1222ba47fc6e702561e7eb7268734db48
added antiquotation @{theory name};

diff -r 223a3de1222b -r 320e136db6dc doc-src/IsarRef/syntax.tex
--- 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