# HG changeset patch
# User nipkow
# Date 1033572331 -7200
# Node ID 9768ba6ab5e79aaf30764b90735fc6cd4ae2bf1f
# Parent  75ae05e894fa084b770e804ce94eedc96c70d466
*** empty log message ***

diff -r 75ae05e894fa -r 9768ba6ab5e7 doc-src/IsarRef/generic.tex
--- a/doc-src/IsarRef/generic.tex	Wed Oct 02 17:03:51 2002 +0200
+++ b/doc-src/IsarRef/generic.tex	Wed Oct 02 17:25:31 2002 +0200
@@ -1223,15 +1223,17 @@
 applies a certain rule in backward fashion, splitting the result into new
 goals with the local contexts being augmented in a purely monotonic manner.
 
-In contrast, $induct$ passes the full goal statement through the ``recursive''
-course involved in the induction.  Thus the original statement is basically
-replaced by separate copies, corresponding to the induction hypotheses and
-conclusion; the original goal context is no longer available.  This behavior
-allows \emph{strengthened induction predicates} to be expressed concisely as
-meta-level rule statements, i.e.\ $\All{\vec x} \vec\phi \Imp \psi$ to
-indicate ``variable'' parameters $\vec x$ and ``recursive'' assumptions
-$\vec\phi$.  Also note that local definitions may be expressed as $\All{\vec
-  x} n \equiv t[\vec x] \Imp \phi[n]$, with induction over $n$.
+In contrast, $induct$ passes the full goal statement through the
+``recursive'' course involved in the induction.  Thus the original statement
+is basically replaced by separate copies, corresponding to the induction
+hypotheses and conclusion; the original goal context is no longer available.
+This behavior allows \emph{strengthened induction predicates} to be expressed
+concisely as meta-level rule statements, i.e.\ $\All{\vec x} \vec\phi \Imp
+\psi$ to indicate ``variable'' parameters $\vec x$ and ``recursive''
+assumptions $\vec\phi$. Note that ``$\isarcmd{case}~c$'' already performs
+``$\FIX{\vec x}$''.  Also note that local definitions may be expressed as
+$\All{\vec x} n \equiv t[\vec x] \Imp \phi[n]$, with induction over $n$.
+
 
 In induction proofs, local assumptions introduced by cases are split into two
 different kinds: $hyps$ stemming from the rule and $prems$ from the goal