--- a/doc-src/IsarRef/Thy/HOL_Specific.thy Mon Nov 23 15:06:34 2009 +0100
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Mon Nov 23 15:06:37 2009 +0100
@@ -452,20 +452,16 @@
\end{description}
- %FIXME check
-
Recursive definitions introduced by the @{command (HOL) "function"}
command accommodate
reasoning by induction (cf.\ \secref{sec:cases-induct}): rule @{text
"c.induct"} (where @{text c} is the name of the function definition)
refers to a specific induction rule, with parameters named according
- to the user-specified equations.
- For the @{command (HOL) "primrec"} the induction principle coincides
+ to the user-specified equations. Cases are numbered (starting from 1).
+
+ For @{command (HOL) "primrec"}, the induction principle coincides
with structural recursion on the datatype the recursion is carried
out.
- Case names of @{command (HOL)
- "primrec"} are that of the datatypes involved, while those of
- @{command (HOL) "function"} are numbered (starting from 1).
The equations provided by these packages may be referred later as
theorem list @{text "f.simps"}, where @{text f} is the (collective)
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Mon Nov 23 15:06:34 2009 +0100
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Mon Nov 23 15:06:37 2009 +0100
@@ -457,18 +457,15 @@
\end{description}
- %FIXME check
-
Recursive definitions introduced by the \hyperlink{command.HOL.function}{\mbox{\isa{\isacommand{function}}}}
command accommodate
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)
refers to a specific induction rule, with parameters named according
- to the user-specified equations.
- For the \hyperlink{command.HOL.primrec}{\mbox{\isa{\isacommand{primrec}}}} the induction principle coincides
+ to the user-specified equations. Cases are numbered (starting from 1).
+
+ For \hyperlink{command.HOL.primrec}{\mbox{\isa{\isacommand{primrec}}}}, the induction principle coincides
with structural recursion on the datatype the recursion is carried
out.
- Case names of \hyperlink{command.HOL.primrec}{\mbox{\isa{\isacommand{primrec}}}} are that of the datatypes involved, while those of
- \hyperlink{command.HOL.function}{\mbox{\isa{\isacommand{function}}}} are numbered (starting from 1).
The equations provided by these packages may be referred later as
theorem list \isa{{\isachardoublequote}f{\isachardot}simps{\isachardoublequote}}, where \isa{f} is the (collective)