--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Sat May 24 22:04:46 2008 +0200
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Sat May 24 22:04:48 2008 +0200
@@ -417,19 +417,16 @@
\indexdef{HOL}{command}{termination}\hypertarget{command.HOL.termination}{\hyperlink{command.HOL.termination}{\mbox{\isa{\isacommand{termination}}}}} & : & \isartrans{local{\dsh}theory}{proof(prove)} \\
\end{matharray}
- \railalias{funopts}{function\_opts} %FIXME ??
-
\begin{rail}
'primrec' target? fixes 'where' equations
;
equations: (thmdecl? prop + '|')
;
- ('fun' | 'function') (funopts)? fixes 'where' clauses
+ ('fun' | 'function') target? functionopts? fixes 'where' clauses
;
clauses: (thmdecl? prop ('(' 'otherwise' ')')? + '|')
;
- funopts: '(' (('sequential' | 'in' name | 'domintros' | 'tailrec' |
- 'default' term) + ',') ')'
+ functionopts: '(' (('sequential' | 'domintros' | 'tailrec' | 'default' term) + ',') ')'
;
'termination' ( term )?
\end{rail}
@@ -493,9 +490,6 @@
may result in several theroems. Also note that this automatic
transformation only works for ML-style datatype patterns.
- \item [\isa{{\isachardoublequote}{\isasymIN}\ name{\isachardoublequote}}] gives the target for the definition.
- %FIXME ?!?
-
\item [\isa{domintros}] enables the automated generation of
introduction rules for the domain predicate. While mostly not
needed, they can be helpful in some proofs about partial functions.