1.1 --- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Sat May 24 20:12:18 2008 +0200
     1.2 +++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Sat May 24 22:04:44 2008 +0200
     1.3 @@ -413,19 +413,16 @@
     1.4      @{command_def (HOL) "termination"} & : & \isartrans{local{\dsh}theory}{proof(prove)} \\
     1.5    \end{matharray}
     1.6  
     1.7 -  \railalias{funopts}{function\_opts}  %FIXME ??
     1.8 -
     1.9    \begin{rail}
    1.10      'primrec' target? fixes 'where' equations
    1.11      ;
    1.12      equations: (thmdecl? prop + '|')
    1.13      ;
    1.14 -    ('fun' | 'function') (funopts)? fixes 'where' clauses
    1.15 +    ('fun' | 'function') target? functionopts? fixes 'where' clauses
    1.16      ;
    1.17      clauses: (thmdecl? prop ('(' 'otherwise' ')')? + '|')
    1.18      ;
    1.19 -    funopts: '(' (('sequential' | 'in' name | 'domintros' | 'tailrec' |
    1.20 -    'default' term) + ',') ')'
    1.21 +    functionopts: '(' (('sequential' | 'domintros' | 'tailrec' | 'default' term) + ',') ')'
    1.22      ;
    1.23      'termination' ( term )?
    1.24    \end{rail}
    1.25 @@ -492,9 +489,6 @@
    1.26    may result in several theroems.  Also note that this automatic
    1.27    transformation only works for ML-style datatype patterns.
    1.28  
    1.29 -  \item [@{text "\<IN> name"}] gives the target for the definition.
    1.30 -  %FIXME ?!?
    1.31 -
    1.32    \item [@{text domintros}] enables the automated generation of
    1.33    introduction rules for the domain predicate. While mostly not
    1.34    needed, they can be helpful in some proofs about partial functions.