1.1 --- a/doc-src/TutorialI/Recdef/Induction.thy	Fri Jan 05 18:32:33 2001 +0100
     1.2 +++ b/doc-src/TutorialI/Recdef/Induction.thy	Fri Jan 05 18:32:57 2001 +0100
     1.3 @@ -16,14 +16,15 @@
     1.4  requires you to prove for each \isacommand{recdef} equation that the property
     1.5  you are trying to establish holds for the left-hand side provided it holds
     1.6  for all recursive calls on the right-hand side. Here is a simple example
     1.7 +involving the predefined @{term"map"} functional on lists:
     1.8  *}
     1.9  
    1.10  lemma "map f (sep(x,xs)) = sep(f x, map f xs)";
    1.11  
    1.12  txt{*\noindent
    1.13 -involving the predefined @{term"map"} functional on lists: @{term"map f xs"}
    1.14 +Note that @{term"map f xs"}
    1.15  is the result of applying @{term"f"} to all elements of @{term"xs"}. We prove
    1.16 -this lemma by recursion induction w.r.t. @{term"sep"}:
    1.17 +this lemma by recursion induction over @{term"sep"}:
    1.18  *}
    1.19  
    1.20  apply(induct_tac x xs rule: sep.induct);
    1.21 @@ -46,7 +47,7 @@
    1.22  
    1.23  In general, the format of invoking recursion induction is
    1.24  \begin{quote}
    1.25 -\isacommand{apply}@{text"(induct_tac ("}$x@1 \dots x@n$ @{text"rule:"} $f$@{text".induct)"}
    1.26 +\isacommand{apply}@{text"(induct_tac "}$x@1 \dots x@n$ @{text"rule:"} $f$@{text".induct)"}
    1.27  \end{quote}\index{*induct_tac}%
    1.28  where $x@1~\dots~x@n$ is a list of free variables in the subgoal and $f$ the
    1.29  name of a function that takes an $n$-tuple. Usually the subgoal will