1.1 --- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Mon Nov 23 15:06:34 2009 +0100
     1.2 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Mon Nov 23 15:06:37 2009 +0100
     1.3 @@ -457,18 +457,15 @@
     1.4  
     1.5    \end{description}
     1.6  
     1.7 -  %FIXME check
     1.8 -
     1.9    Recursive definitions introduced by the \hyperlink{command.HOL.function}{\mbox{\isa{\isacommand{function}}}}
    1.10    command accommodate
    1.11    reasoning by induction (cf.\ \secref{sec:cases-induct}): rule \isa{{\isachardoublequote}c{\isachardot}induct{\isachardoublequote}} (where \isa{c} is the name of the function definition)
    1.12    refers to a specific induction rule, with parameters named according
    1.13 -  to the user-specified equations.
    1.14 -  For the \hyperlink{command.HOL.primrec}{\mbox{\isa{\isacommand{primrec}}}} the induction principle coincides
    1.15 +  to the user-specified equations. Cases are numbered (starting from 1).
    1.16 +
    1.17 +  For \hyperlink{command.HOL.primrec}{\mbox{\isa{\isacommand{primrec}}}}, the induction principle coincides
    1.18    with structural recursion on the datatype the recursion is carried
    1.19    out.
    1.20 -  Case names of \hyperlink{command.HOL.primrec}{\mbox{\isa{\isacommand{primrec}}}} are that of the datatypes involved, while those of
    1.21 -  \hyperlink{command.HOL.function}{\mbox{\isa{\isacommand{function}}}} are numbered (starting from 1).
    1.22  
    1.23    The equations provided by these packages may be referred later as
    1.24    theorem list \isa{{\isachardoublequote}f{\isachardot}simps{\isachardoublequote}}, where \isa{f} is the (collective)