doc-src/IsarRef/generic.tex

--- a/doc-src/IsarRef/generic.tex	Fri Sep 03 16:11:03 1999 +0200
+++ b/doc-src/IsarRef/generic.tex	Fri Sep 03 16:11:53 1999 +0200
@@ -4,12 +4,11 @@
 \section{Basic proof methods}\label{sec:pure-meth}
 
 \indexisarmeth{fail}\indexisarmeth{succeed}\indexisarmeth{$-$}\indexisarmeth{assumption}
-\indexisarmeth{finish}\indexisarmeth{fold}\indexisarmeth{unfold}
+\indexisarmeth{fold}\indexisarmeth{unfold}
 \indexisarmeth{rule}\indexisarmeth{erule}
 \begin{matharray}{rcl}
   - & : & \isarmeth \\
   assumption & : & \isarmeth \\
-  finish & : & \isarmeth \\[0.5ex]
   rule & : & \isarmeth \\
   erule^* & : & \isarmeth \\[0.5ex]
   fold & : & \isarmeth \\
@@ -29,11 +28,8 @@
   performs a single reduction step using the $rule$ method (see below); thus a
   plain \emph{do-nothing} proof step would be $\PROOF{-}$ rather than
   $\PROOFNAME$ alone.
-\item [$assumption$] solves some goal by assumption, after inserting the
-  goal's facts.
-\item [$finish$] solves all remaining goals by assumption; this is the default
-  terminal proof method for $\QEDNAME$, i.e.\ it usually does not have to be
-  spelled out explicitly.
+\item [$assumption$] solves some goal by assumption.  The facts (if any) are
+  guaranteed to participate.
 \item [$rule~thms$] applies some rule given as argument in backward manner;
   facts are used to reduce the rule before applying it to the goal.  Thus
   $rule$ without facts is plain \emph{introduction}, while with facts it
@@ -142,7 +138,7 @@
 Calculational proof is forward reasoning with implicit application of
 transitivity rules (such those of $=$, $\le$, $<$).  Isabelle/Isar maintains
 an auxiliary register $calculation$\indexisarthm{calculation} for accumulating
-results obtained by transitivity obtained together with the current facts.
+results obtained by transitivity obtained together with the current result.
 Command $\ALSO$ updates $calculation$ from the most recent result, while
 $\FINALLY$ exhibits the final result by forward chaining towards the next goal
 statement.  Both commands require valid current facts, i.e.\ may occur only
@@ -173,11 +169,11 @@
 \begin{descr}
 \item [$\ALSO~(thms)$] maintains the auxiliary $calculation$ register as
   follows.  The first occurrence of $\ALSO$ in some calculational thread
-  initialises $calculation$ by $facts$. Any subsequent $\ALSO$ on the same
+  initialises $calculation$ by $this$. Any subsequent $\ALSO$ on the same
   level of block-structure updates $calculation$ by some transitivity rule
-  applied to $calculation$ and $facts$ (in that order).  Transitivity rules
-  are picked from the current context plus those given as $thms$ (the latter
-  have precedence).
+  applied to $calculation$ and $this$ (in that order).  Transitivity rules are
+  picked from the current context plus those given as $thms$ (the latter have
+  precedence).
   
 \item [$\FINALLY~(thms)$] maintaining $calculation$ in the same way as
   $\ALSO$, and concludes the current calculational thread.  The final result
@@ -343,9 +339,10 @@
   actually happens, thus it is very appropriate as an initial method for
   $\PROOFNAME$ that splits up certain connectives of the goal, before entering
   the sub-proof.
-
-\item [Method $contradiction$] solves some goal by contradiction: both $A$ and
-  $\neg A$ have to be present in the assumptions.
+  
+\item [Method $contradiction$] solves some goal by contradiction, deriving any
+  result from both $\neg A$ and $A$.  Facts, which are guaranteed to
+  participate, may appear in either order.
 \end{descr}