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