clarified; checked
authorkrauss
Mon Nov 23 15:06:37 2009 +0100 (2009-11-23)
changeset 338570cb5002c52db
parent 33856 14a658faadb6
child 33858 0c348f7997f7
clarified; checked
doc-src/IsarRef/Thy/HOL_Specific.thy
doc-src/IsarRef/Thy/document/HOL_Specific.tex
     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)
     2.1 --- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Mon Nov 23 15:06:34 2009 +0100
     2.2 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Mon Nov 23 15:06:37 2009 +0100
     2.3 @@ -457,18 +457,15 @@
     2.4  
     2.5    \end{description}
     2.6  
     2.7 -  %FIXME check
     2.8 -
     2.9    Recursive definitions introduced by the \hyperlink{command.HOL.function}{\mbox{\isa{\isacommand{function}}}}
    2.10    command accommodate
    2.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)
    2.12    refers to a specific induction rule, with parameters named according
    2.13 -  to the user-specified equations.
    2.14 -  For the \hyperlink{command.HOL.primrec}{\mbox{\isa{\isacommand{primrec}}}} the induction principle coincides
    2.15 +  to the user-specified equations. Cases are numbered (starting from 1).
    2.16 +
    2.17 +  For \hyperlink{command.HOL.primrec}{\mbox{\isa{\isacommand{primrec}}}}, the induction principle coincides
    2.18    with structural recursion on the datatype the recursion is carried
    2.19    out.
    2.20 -  Case names of \hyperlink{command.HOL.primrec}{\mbox{\isa{\isacommand{primrec}}}} are that of the datatypes involved, while those of
    2.21 -  \hyperlink{command.HOL.function}{\mbox{\isa{\isacommand{function}}}} are numbered (starting from 1).
    2.22  
    2.23    The equations provided by these packages may be referred later as
    2.24    theorem list \isa{{\isachardoublequote}f{\isachardot}simps{\isachardoublequote}}, where \isa{f} is the (collective)