1.1 --- a/doc-src/IsarRef/pure.tex Sun Oct 31 15:20:35 1999 +0100
1.2 +++ b/doc-src/IsarRef/pure.tex Sun Oct 31 15:25:55 1999 +0100
1.3 @@ -804,8 +804,8 @@
1.4 but part of others (such as $\ASSUMENAME$, $\HAVENAME$ etc.).
1.5 \end{descr}
1.6
1.7 -A few \emph{automatic} term abbreviations\index{automatic abbreviation} for
1.8 -goals and facts are available as well. For any open goal,
1.9 +A few \emph{automatic} term abbreviations\index{term abbreviations} for goals
1.10 +and facts are available as well. For any open goal,
1.11 $\Var{thesis_prop}$\indexisarvar{thesis-prop} refers to the full proposition
1.12 (which may be a rule), $\Var{thesis_concl}$\indexisarvar{thesis-concl} to its
1.13 (atomic) conclusion, and $\Var{thesis}$\indexisarvar{thesis} to its