diff -r f3ff2549cdc8 -r 23a118849801 doc-src/TutorialI/Inductive/even-example.tex
--- a/doc-src/TutorialI/Inductive/even-example.tex	Thu Aug 09 10:17:45 2001 +0200
+++ b/doc-src/TutorialI/Inductive/even-example.tex	Thu Aug 09 18:12:15 2001 +0200
@@ -27,7 +27,7 @@
 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,
-thus following the definitional approach (see \S\ref{sec:definitional}).
+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
@@ -300,9 +300,10 @@
 dispensing with the lemma \isa{even_imp_even_minus_2}. 
 This example also justifies the terminology
 \textbf{rule inversion}: the new rule inverts the introduction rule
-\isa{even.step}.
+\isa{even.step}.  In general, a rule can be inverted when the set of elements
+it introduces is disjoint from those of the other introduction rules.
 
-For one-off applications of rule inversion, use the \isa{ind_cases} method. 
+For one-off applications of rule inversion, use the \methdx{ind_cases} method. 
 Here is an example:
 \begin{isabelle}
 \isacommand{apply}\ (ind_cases\ "Suc(Suc\ n)\ \isasymin \ even")