diff -r 813a4e8f1276 -r 770356c32ad9 doc-src/IsarRef/syntax.tex
--- 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