1.1 --- a/doc-src/TutorialI/Misc/AdvancedInd.thy	Wed Oct 18 12:30:59 2000 +0200
     1.2 +++ b/doc-src/TutorialI/Misc/AdvancedInd.thy	Wed Oct 18 17:19:18 2000 +0200
     1.3 @@ -34,13 +34,14 @@
     1.4  \begin{isabelle}
     1.5  \ 1.\ xs\ {\isasymnoteq}\ []\ {\isasymLongrightarrow}\ hd\ []\ =\ last\ []
     1.6  \end{isabelle}
     1.7 -We cannot prove this equality because we do not know what @{term"hd"} and
     1.8 -@{term"last"} return when applied to @{term"[]"}.
     1.9 +We cannot prove this equality because we do not know what @{term hd} and
    1.10 +@{term last} return when applied to @{term"[]"}.
    1.11  
    1.12  The point is that we have violated the above warning. Because the induction
    1.13 -formula is only the conclusion, the occurrence of @{term"xs"} in the premises is
    1.14 +formula is only the conclusion, the occurrence of @{term xs} in the premises is
    1.15  not modified by induction. Thus the case that should have been trivial
    1.16 -becomes unprovable. Fortunately, the solution is easy:
    1.17 +becomes unprovable. Fortunately, the solution is easy:\footnote{A very similar
    1.18 +heuristic applies to rule inductions; see \S\ref{sec:rtc}.}
    1.19  \begin{quote}
    1.20  \emph{Pull all occurrences of the induction variable into the conclusion
    1.21  using @{text"\<longrightarrow>"}.}