--- a/doc-src/IsarRef/Thy/HOL_Specific.thy Tue Oct 26 12:19:01 2010 +0200
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Tue Oct 26 12:19:01 2010 +0200
@@ -401,11 +401,9 @@
\begin{rail}
'primrec' target? fixes 'where' equations
;
- equations: (thmdecl? prop + '|')
+ ('fun' | 'function') target? functionopts? fixes \\ 'where' equations
;
- ('fun' | 'function') target? functionopts? fixes 'where' clauses
- ;
- clauses: (thmdecl? prop ('(' 'otherwise' ')')? + '|')
+ equations: (thmdecl? prop + '|')
;
functionopts: '(' (('sequential' | 'domintros' | 'tailrec' | 'default' term) + ',') ')'
;
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Tue Oct 26 12:19:01 2010 +0200
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Tue Oct 26 12:19:01 2010 +0200
@@ -411,11 +411,9 @@
\begin{rail}
'primrec' target? fixes 'where' equations
;
- equations: (thmdecl? prop + '|')
+ ('fun' | 'function') target? functionopts? fixes \\ 'where' equations
;
- ('fun' | 'function') target? functionopts? fixes 'where' clauses
- ;
- clauses: (thmdecl? prop ('(' 'otherwise' ')')? + '|')
+ equations: (thmdecl? prop + '|')
;
functionopts: '(' (('sequential' | 'domintros' | 'tailrec' | 'default' term) + ',') ')'
;