1.1 --- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Thu Jul 03 00:58:30 2008 +0200
     1.2 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Thu Jul 03 11:16:05 2008 +0200
     1.3 @@ -365,20 +365,18 @@
     1.4  \begin{isamarkuptext}%
     1.5  \begin{matharray}{rcl}
     1.6      \indexdef{HOL}{command}{datatype}\hypertarget{command.HOL.datatype}{\hyperlink{command.HOL.datatype}{\mbox{\isa{\isacommand{datatype}}}}} & : & \isartrans{theory}{theory} \\
     1.7 -    \indexdef{HOL}{command}{rep\_datatype}\hypertarget{command.HOL.rep-datatype}{\hyperlink{command.HOL.rep-datatype}{\mbox{\isa{\isacommand{rep{\isacharunderscore}datatype}}}}} & : & \isartrans{theory}{theory} \\
     1.8 +  \indexdef{HOL}{command}{rep\_datatype}\hypertarget{command.HOL.rep-datatype}{\hyperlink{command.HOL.rep-datatype}{\mbox{\isa{\isacommand{rep{\isacharunderscore}datatype}}}}} & : & \isartrans{theory}{proof} \\
     1.9    \end{matharray}
    1.10  
    1.11    \begin{rail}
    1.12      'datatype' (dtspec + 'and')
    1.13      ;
    1.14 -    'rep\_datatype' (name *) dtrules
    1.15 +    'rep\_datatype' ('(' (name +) ')')? (term +)
    1.16      ;
    1.17  
    1.18      dtspec: parname? typespec infix? '=' (cons + '|')
    1.19      ;
    1.20      cons: name (type *) mixfix?
    1.21 -    ;
    1.22 -    dtrules: 'distinct' thmrefs 'inject' thmrefs 'induction' thmrefs
    1.23    \end{rail}
    1.24  
    1.25    \begin{descr}
    1.26 @@ -464,10 +462,15 @@
    1.27  
    1.28    %FIXME check
    1.29  
    1.30 -  Recursive definitions introduced by both the \hyperlink{command.HOL.primrec}{\mbox{\isa{\isacommand{primrec}}}} and the \hyperlink{command.HOL.function}{\mbox{\isa{\isacommand{function}}}} command accommodate
    1.31 +  Recursive definitions introduced by the \hyperlink{command.HOL.function}{\mbox{\isa{\isacommand{function}}}}
    1.32 +  command accommodate
    1.33    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)
    1.34    refers to a specific induction rule, with parameters named according
    1.35 -  to the user-specified equations.  Case names of \hyperlink{command.HOL.primrec}{\mbox{\isa{\isacommand{primrec}}}} are that of the datatypes involved, while those of
    1.36 +  to the user-specified equations.
    1.37 +  For the \hyperlink{command.HOL.primrec}{\mbox{\isa{\isacommand{primrec}}}} the induction principle coincides
    1.38 +  with structural recursion on the datatype the recursion is carried
    1.39 +  out.
    1.40 +  Case names of \hyperlink{command.HOL.primrec}{\mbox{\isa{\isacommand{primrec}}}} are that of the datatypes involved, while those of
    1.41    \hyperlink{command.HOL.function}{\mbox{\isa{\isacommand{function}}}} are numbered (starting from 1).
    1.42  
    1.43    The equations provided by these packages may be referred later as
    1.44 @@ -988,7 +991,7 @@
    1.45      'code\_modulename' target ( ( string string ) + )
    1.46      ;
    1.47  
    1.48 -    'code\_exception' ( const + )
    1.49 +    'code\_abort' ( const + )
    1.50      ;
    1.51  
    1.52      syntax: string | ( 'infix' | 'infixl' | 'infixr' ) nat string
    1.53 @@ -1075,13 +1078,13 @@
    1.54    one module name onto another.
    1.55  
    1.56    \item [\hyperlink{command.HOL.code-abort}{\mbox{\isa{\isacommand{code{\isacharunderscore}abort}}}}] declares constants which
    1.57 -  are not required to have a definition by a defining equations;
    1.58 +  are not required to have a definition by means of defining equations;
    1.59    if needed these are implemented by program abort instead.
    1.60  
    1.61    \item [\hyperlink{attribute.HOL.code}{\mbox{\isa{code}}}~\isa{func}] explicitly selects (or
    1.62    with option ``\isa{{\isachardoublequote}del{\isacharcolon}{\isachardoublequote}}'' deselects) a defining equation for
    1.63    code generation.  Usually packages introducing defining equations
    1.64 -  provide a resonable default setup for selection.
    1.65 +  provide a reasonable default setup for selection.
    1.66  
    1.67    \item [\hyperlink{attribute.HOL.code}{\mbox{\isa{code}}}\isa{inline}] declares (or with
    1.68    option ``\isa{{\isachardoublequote}del{\isacharcolon}{\isachardoublequote}}'' removes) inlining theorems which are