1.1 --- a/doc-src/TutorialI/Misc/AdvancedInd.thy	Tue May 01 17:16:32 2001 +0200
     1.2 +++ b/doc-src/TutorialI/Misc/AdvancedInd.thy	Tue May 01 22:26:55 2001 +0200
     1.3 @@ -86,7 +86,9 @@
     1.4  you want to induct on a whole term, rather than an individual variable. In
     1.5  general, when inducting on some term $t$ you must rephrase the conclusion $C$
     1.6  as
     1.7 -\[ \forall y@1 \dots y@n.~ x = t \longrightarrow C \]
     1.8 +\begin{equation}\label{eqn:ind-over-term}
     1.9 +\forall y@1 \dots y@n.~ x = t \longrightarrow C
    1.10 +\end{equation}
    1.11  where $y@1 \dots y@n$ are the free variables in $t$ and $x$ is new, and
    1.12  perform induction on $x$ afterwards. An example appears in
    1.13  \S\ref{sec:complete-ind} below.
    1.14 @@ -101,7 +103,20 @@
    1.15  
    1.16  Of course, all premises that share free variables with $t$ need to be pulled into
    1.17  the conclusion as well, under the @{text"\<forall>"}, again using @{text"\<longrightarrow>"} as shown above.
    1.18 -*};
    1.19 +
    1.20 +Readers who are puzzled by the form of statement
    1.21 +(\ref{eqn:ind-over-term}) above should remember that the
    1.22 +transformation is only performed to permit induction. Once induction
    1.23 +has been applied, the statement can be transformed back into something quite
    1.24 +intuitive. For example, applying wellfounded induction on $x$ (w.r.t.\
    1.25 +$\prec$) to (\ref{eqn:ind-over-term}) and transforming the result a
    1.26 +little leads to the goal
    1.27 +\[ \bigwedge\vec{y}.~\forall \vec{z}.~ t(\vec{z}) \prec t(\vec{y}) \longrightarrow C(\vec{z})
    1.28 +   \Longrightarrow C(\vec{y}) \]
    1.29 +where the dependence of $t$ and $C$ on their free variables has been made explicit.
    1.30 +Unfortunately, this induction schema cannot be expressed as a single theorem because it depends
    1.31 +on the number of free variables in $t$ --- the notation $\vec{y}$ is merely an informal device.
    1.32 +*}
    1.33  
    1.34  subsection{*Beyond Structural and Recursion Induction*};
    1.35