--- a/doc-src/IsarRef/syntax.tex Mon Oct 30 08:34:37 2000 +0100
+++ b/doc-src/IsarRef/syntax.tex Mon Oct 30 08:40:05 2000 +0100
@@ -344,6 +344,7 @@
typ & : & \isarantiq \\
text & : & \isarantiq \\
goals & : & \isarantiq \\
+ subgoals & : & \isarantiq \\
\end{matharray}
The text body of formal comments (see also \S\ref{sec:comments}) may contain
@@ -402,6 +403,8 @@
Please do not include goal states into document output unless you really
know what you are doing!
+\item [$\at\{subgoals\}$] behaves almost like $goals$, except that it does
+ not print the overall goal.
\end{descr}
\medskip