--- 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