--- a/doc-src/IsarRef/pure.tex Mon Aug 30 14:07:48 1999 +0200
+++ b/doc-src/IsarRef/pure.tex Mon Aug 30 14:08:23 1999 +0200
@@ -498,7 +498,7 @@
resulting hypothetical equation solved by reflexivity.
\end{descr}
-The special theorem name $prems$\indexisarreg{prems} refers to all current
+The special theorem name $prems$\indexisarthm{prems} refers to all current
assumptions.
@@ -516,7 +516,7 @@
Any fact will usually be involved in further proofs, either as explicit
arguments of proof methods or when forward chaining towards the next goal via
$\THEN$ (and variants). Note that the special theorem name
-$facts$.\indexisarreg{facts} refers to the most recently established facts.
+$facts$.\indexisarthm{facts} refers to the most recently established facts.
\begin{rail}
'note' thmdef? thmrefs comment?
;
@@ -541,6 +541,13 @@
chaining is from earlier facts together with the current ones.
\end{descr}
+Basic proof methods (such as $rule$, see \S\ref{sec:pure-meth}) expect
+multiple facts to be given in proper order, corresponding to a prefix of the
+premises of the rule involved. Note that positions may be easily skipped
+using a form like $\FROM{_~a~b}$, for example. This involves the rule
+$PROP~\psi \Imp PROP~\psi$, which is bound in Isabelle/Pure as ``_''
+(underscore).\indexisarthm{_@\texttt{_}}
+
\subsection{Goal statements}
@@ -702,8 +709,9 @@
\item [$\isarkeyword{then_apply}~(m)$] is similar to $\isarkeyword{apply}$,
but observes the goal's facts.
\item [$\isarkeyword{back}$] does back-tracking over the result sequence of
- the last proof command. Basically, any proof command may return multiple
- results.
+ the latest proof command.\footnote{Unlike the ML function \texttt{back}
+ \cite{isabelle-ref}, the Isar command does not search upwards for further
+ branch points.} Basically, any proof command may return multiple results.
\end{descr}