# HG changeset patch
# User krauss
# Date 1258985197 -3600
# Node ID 0cb5002c52dbcdc5c7eb724de0cc43d71225cf66
# Parent  14a658faadb6bb2d75191bd09ba5a2f1555f6406
clarified; checked

diff -r 14a658faadb6 -r 0cb5002c52db doc-src/IsarRef/Thy/HOL_Specific.thy
--- 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)
diff -r 14a658faadb6 -r 0cb5002c52db doc-src/IsarRef/Thy/document/HOL_Specific.tex
--- 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)