--- a/doc-src/IsarRef/pure.tex Fri May 26 18:28:15 2000 +0200
+++ b/doc-src/IsarRef/pure.tex Sun May 28 21:55:50 2000 +0200
@@ -681,6 +681,12 @@
also equivalent to $\FROM{this}~\SHOWNAME$.
\end{descr}
+Note that any goal statement causes some term abbreviations (such as
+$\Var{thesis}$, $\dots$) to be bound automatically, see also
+\S\ref{sec:term-abbrev}. Furthermore, the local context of a (non-atomic)
+goal is provided via the case name $antecedent$\indexisarcase{antecedent}, see
+also \S\ref{sec:cases}.
+
\subsection{Initial and terminal proof steps}\label{sec:proof-steps}