# HG changeset patch
# User wenzelm
# Date 972926614 -3600
# Node ID aef4f587a0e4f26239988fda005c305b680bb903
# Parent  ae236e935a3461e5fe8cc468bd4e00de716c38d8
improved doc of "subgoals" antiquotation;

diff -r ae236e935a34 -r aef4f587a0e4 doc-src/IsarRef/syntax.tex
--- a/doc-src/IsarRef/syntax.tex	Mon Oct 30 18:22:49 2000 +0100
+++ b/doc-src/IsarRef/syntax.tex	Mon Oct 30 18:23:34 2000 +0100
@@ -363,7 +363,7 @@
 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
   ;
@@ -374,7 +374,8 @@
     'term' options term |
     'typ' options type |
     'text' options name |
-    'goals' options
+    'goals' options |
+    'subgoals' options
   ;
   options: '[' (option * ',') ']'
   ;
@@ -403,8 +404,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.
+\item [$\at\{subgoals\}$] behaves almost like $goals$, except that it does not
+  print the main goal.
 \end{descr}
 
 \medskip