# HG changeset patch
# User wenzelm
# Date 936014903 -7200
# Node ID f647f463abebfd1d94568dc82d20a607ecbab40c
# Parent  df8490c9a674508db8349d51f36698471775cffa
'_' theorem;
back: only latest command;

diff -r df8490c9a674 -r f647f463abeb doc-src/IsarRef/pure.tex
--- 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}