diff -r f43fa07536c0 -r eddc69b55fac doc-src/TutorialI/Inductive/even-example.tex
--- a/doc-src/TutorialI/Inductive/even-example.tex	Fri Mar 09 19:05:48 2001 +0100
+++ b/doc-src/TutorialI/Inductive/even-example.tex	Mon Mar 12 18:17:45 2001 +0100
@@ -25,7 +25,9 @@
 An inductive definition consists of introduction rules.  The first one
 above states that 0 is even; the second states that if $n$ is even, then so
 is~$n+2$.  Given this declaration, Isabelle generates a fixed point
-definition for \isa{even} and proves theorems about it.  These theorems
+definition for \isa{even} and proves theorems about it,
+thus following the definitional approach (see \S\ref{sec:definitional}).
+These theorems
 include the introduction rules specified in the declaration, an elimination
 rule for case analysis and an induction rule.  We can refer to these
 theorems by automatically-generated names.  Here are two examples: