doc-src/IsarRef/Thy/HOL_Specific.thy
changeset 40170 751121d5ca35
parent 39608 76bc7e4999f8
child 40171 1fa547166a1d
     1.1 --- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Tue Oct 26 12:19:01 2010 +0200
     1.2 +++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Tue Oct 26 12:19:01 2010 +0200
     1.3 @@ -401,11 +401,9 @@
     1.4    \begin{rail}
     1.5      'primrec' target? fixes 'where' equations
     1.6      ;
     1.7 -    equations: (thmdecl? prop + '|')
     1.8 +    ('fun' | 'function') target? functionopts? fixes \\ 'where' equations
     1.9      ;
    1.10 -    ('fun' | 'function') target? functionopts? fixes 'where' clauses
    1.11 -    ;
    1.12 -    clauses: (thmdecl? prop ('(' 'otherwise' ')')? + '|')
    1.13 +    equations: (thmdecl? prop + '|')
    1.14      ;
    1.15      functionopts: '(' (('sequential' | 'domintros' | 'tailrec' | 'default' term) + ',') ')'
    1.16      ;