doc-src/IsarRef/syntax.tex

 \texttt{{\at}{\ttlbrace}thm~sym~[no_vars]{\ttrbrace}} would print the
 statement where all schematic variables have been replaced by fixed ones,
 which are better readable.
 
 \indexisarant{thm}\indexisarant{prop}\indexisarant{term}
-\indexisarant{typ}\indexisarant{text}\indexisarant{goals}
+\indexisarant{typ}\indexisarant{text}\indexisarant{goals}\indexisarant{subgoals}
 \begin{rail}
   atsign lbrace antiquotation rbrace
   ;
 
   antiquotation:
     'thm' options thmrefs |
     'prop' options prop |
     'term' options term |
     'typ' options type |
     'text' options name |
-    'goals' options
+    'goals' options |
+    'subgoals' options
   ;
   options: '[' (option * ',') ']'
   ;
   option: name | name '=' name
   ;

   only for support of tactic-emulation scripts within Isar --- presentation of
   goal states does not conform to actual human-readable proof documents.
   
   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.
+\item [$\at\{subgoals\}$] behaves almost like $goals$, except that it does not
+  print the main goal.
 \end{descr}
 
 \medskip
 
 The following options are available to tune the output.  Note that most of