1.1 --- a/doc-src/TutorialI/Recdef/document/Induction.tex	Fri Sep 01 18:29:52 2000 +0200
     1.2 +++ b/doc-src/TutorialI/Recdef/document/Induction.tex	Fri Sep 01 19:09:44 2000 +0200
     1.3 @@ -9,7 +9,7 @@
     1.4  again induction. But this time the structural form of induction that comes
     1.5  with datatypes is unlikely to work well---otherwise we could have defined the
     1.6  function by \isacommand{primrec}. Therefore \isacommand{recdef} automatically
     1.7 -proves a suitable induction rule $f$\isa{.induct} that follows the
     1.8 +proves a suitable induction rule $f$\isa{{\isachardot}induct} that follows the
     1.9  recursion pattern of the particular function $f$. We call this
    1.10  \textbf{recursion induction}. Roughly speaking, it
    1.11  requires you to prove for each \isacommand{recdef} equation that the property
    1.12 @@ -19,7 +19,7 @@
    1.13  \isacommand{lemma}\ {\isachardoublequote}map\ f\ {\isacharparenleft}sep{\isacharparenleft}x{\isacharcomma}xs{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ sep{\isacharparenleft}f\ x{\isacharcomma}\ map\ f\ xs{\isacharparenright}{\isachardoublequote}%
    1.14  \begin{isamarkuptxt}%
    1.15  \noindent
    1.16 -involving the predefined \isa{map} functional on lists: \isa{map f xs}
    1.17 +involving the predefined \isa{map} functional on lists: \isa{map\ f\ xs}
    1.18  is the result of applying \isa{f} to all elements of \isa{xs}. We prove
    1.19  this lemma by recursion induction w.r.t. \isa{sep}:%
    1.20  \end{isamarkuptxt}%
    1.21 @@ -45,13 +45,13 @@
    1.22  definition of \isa{sep}.
    1.23  
    1.24  In general, the format of invoking recursion induction is
    1.25 -\begin{ttbox}
    1.26 -apply(induct_tac \(x@1 \dots x@n\) rule: \(f\).induct)
    1.27 -\end{ttbox}\index{*induct_tac}%
    1.28 +\begin{quote}
    1.29 +\isacommand{apply}\isa{{\isacharparenleft}induct{\isacharunderscore}tac\ {\isacharparenleft}}$x@1 \dots x@n$ \isa{rule{\isacharcolon}} $f$\isa{{\isachardot}induct{\isacharparenright}}
    1.30 +\end{quote}\index{*induct_tac}%
    1.31  where $x@1~\dots~x@n$ is a list of free variables in the subgoal and $f$ the
    1.32  name of a function that takes an $n$-tuple. Usually the subgoal will
    1.33  contain the term $f~x@1~\dots~x@n$ but this need not be the case. The
    1.34 -induction rules do not mention $f$ at all. For example \isa{sep.induct}
    1.35 +induction rules do not mention $f$ at all. For example \isa{sep{\isachardot}induct}
    1.36  \begin{isabelle}
    1.37  {\isasymlbrakk}~{\isasymAnd}a.~P~a~[];\isanewline
    1.38  ~~{\isasymAnd}a~x.~P~a~[x];\isanewline