doc-src/TutorialI/Inductive/Even.tex
changeset 10520 bb9dfcc87951
parent 10419 1bfdd19c1d47
child 10654 458068404143
     1.1 --- a/doc-src/TutorialI/Inductive/Even.tex	Fri Nov 24 16:49:27 2000 +0100
     1.2 +++ b/doc-src/TutorialI/Inductive/Even.tex	Sun Nov 26 10:48:38 2000 +0100
     1.3 @@ -157,6 +157,7 @@
     1.4  \end{isabelle}
     1.5  
     1.6  \subsection{Generalization and rule induction}
     1.7 +\label{sec:gen-rule-induction}
     1.8  
     1.9  Everybody knows that when before applying induction we often must generalize
    1.10  the induction formula.  This step is just as important with rule induction,