author | krauss |

Mon Nov 23 15:06:37 2009 +0100 (2009-11-23) | |

changeset 33857 | 0cb5002c52db |

parent 33856 | 14a658faadb6 |

child 33858 | 0c348f7997f7 |

clarified; checked

doc-src/IsarRef/Thy/HOL_Specific.thy | file | annotate | diff | revisions | |

doc-src/IsarRef/Thy/document/HOL_Specific.tex | file | annotate | diff | revisions |

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)