doc-src/TutorialI/Recdef/document/Induction.tex
changeset 10971 6852682eaf16
parent 10950 aa788fcb75a5
child 11023 6e6c8d1ec89e
     1.1 --- a/doc-src/TutorialI/Recdef/document/Induction.tex	Wed Jan 24 11:59:15 2001 +0100
     1.2 +++ b/doc-src/TutorialI/Recdef/document/Induction.tex	Wed Jan 24 12:29:10 2001 +0100
     1.3 @@ -8,7 +8,7 @@
     1.4  equations) are simplification rules, we might like to prove something about
     1.5  our function. Since the function is recursive, the natural proof principle is
     1.6  again induction. But this time the structural form of induction that comes
     1.7 -with datatypes is unlikely to work well---otherwise we could have defined the
     1.8 +with datatypes is unlikely to work well --- otherwise we could have defined the
     1.9  function by \isacommand{primrec}. Therefore \isacommand{recdef} automatically
    1.10  proves a suitable induction rule $f$\isa{{\isachardot}induct} that follows the
    1.11  recursion pattern of the particular function $f$. We call this
    1.12 @@ -53,7 +53,7 @@
    1.13  \end{quote}\index{*induct_tac}%
    1.14  where $x@1~\dots~x@n$ is a list of free variables in the subgoal and $f$ the
    1.15  name of a function that takes an $n$-tuple. Usually the subgoal will
    1.16 -contain the term $f~x@1~\dots~x@n$ but this need not be the case. The
    1.17 +contain the term $f(x@1,\dots,x@n)$ but this need not be the case. The
    1.18  induction rules do not mention $f$ at all. For example \isa{sep{\isachardot}induct}
    1.19  \begin{isabelle}
    1.20  {\isasymlbrakk}~{\isasymAnd}a.~P~a~[];\isanewline