doc-src/IsarRef/Thy/HOL_Specific.thy
changeset 27452 5c1fb7d262bf
parent 27123 11fcdd5897dd
child 27706 10a6ede68bc8
     1.1 --- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Thu Jul 03 00:58:30 2008 +0200
     1.2 +++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Thu Jul 03 11:16:05 2008 +0200
     1.3 @@ -362,20 +362,18 @@
     1.4  text {*
     1.5    \begin{matharray}{rcl}
     1.6      @{command_def (HOL) "datatype"} & : & \isartrans{theory}{theory} \\
     1.7 -    @{command_def (HOL) "rep_datatype"} & : & \isartrans{theory}{theory} \\
     1.8 +  @{command_def (HOL) "rep_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 @@ -460,12 +458,16 @@
    1.27  
    1.28    %FIXME check
    1.29  
    1.30 -  Recursive definitions introduced by both the @{command (HOL)
    1.31 -  "primrec"} and the @{command (HOL) "function"} command accommodate
    1.32 +  Recursive definitions introduced by the @{command (HOL) "function"}
    1.33 +  command accommodate
    1.34    reasoning by induction (cf.\ \secref{sec:cases-induct}): rule @{text
    1.35    "c.induct"} (where @{text c} is the name of the function definition)
    1.36    refers to a specific induction rule, with parameters named according
    1.37 -  to the user-specified equations.  Case names of @{command (HOL)
    1.38 +  to the user-specified equations.
    1.39 +  For the @{command (HOL) "primrec"} the induction principle coincides
    1.40 +  with structural recursion on the datatype the recursion is carried
    1.41 +  out.
    1.42 +  Case names of @{command (HOL)
    1.43    "primrec"} are that of the datatypes involved, while those of
    1.44    @{command (HOL) "function"} are numbered (starting from 1).
    1.45  
    1.46 @@ -985,7 +987,7 @@
    1.47      'code\_modulename' target ( ( string string ) + )
    1.48      ;
    1.49  
    1.50 -    'code\_exception' ( const + )
    1.51 +    'code\_abort' ( const + )
    1.52      ;
    1.53  
    1.54      syntax: string | ( 'infix' | 'infixl' | 'infixr' ) nat string
    1.55 @@ -1075,13 +1077,13 @@
    1.56    one module name onto another.
    1.57  
    1.58    \item [@{command (HOL) "code_abort"}] declares constants which
    1.59 -  are not required to have a definition by a defining equations;
    1.60 +  are not required to have a definition by means of defining equations;
    1.61    if needed these are implemented by program abort instead.
    1.62  
    1.63    \item [@{attribute (HOL) code}~@{text func}] explicitly selects (or
    1.64    with option ``@{text "del:"}'' deselects) a defining equation for
    1.65    code generation.  Usually packages introducing defining equations
    1.66 -  provide a resonable default setup for selection.
    1.67 +  provide a reasonable default setup for selection.
    1.68  
    1.69    \item [@{attribute (HOL) code}@{text inline}] declares (or with
    1.70    option ``@{text "del:"}'' removes) inlining theorems which are