doc-src/IsarRef/Thy/document/HOL_Specific.tex
changeset 26987 978cefd606ad
parent 26907 75466ad27dd7
child 27042 8fcf19f2168b
     1.1 --- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Sat May 24 22:04:46 2008 +0200
     1.2 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Sat May 24 22:04:48 2008 +0200
     1.3 @@ -417,19 +417,16 @@
     1.4      \indexdef{HOL}{command}{termination}\hypertarget{command.HOL.termination}{\hyperlink{command.HOL.termination}{\mbox{\isa{\isacommand{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 @@ -493,9 +490,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 [\isa{{\isachardoublequote}{\isasymIN}\ name{\isachardoublequote}}] gives the target for the definition.
    1.30 -  %FIXME ?!?
    1.31 -
    1.32    \item [\isa{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.