# HG changeset patch # User wenzelm # Date 1211659484 -7200 # Node ID 51c5acd57b756ac22badcc74badbac484e020356 # Parent d0e098e206f39b9ba99e8342ab8e5609166ce8c9 function: uniform treatment of target, not as config; diff -r d0e098e206f3 -r 51c5acd57b75 doc-src/IsarRef/Thy/HOL_Specific.thy --- a/doc-src/IsarRef/Thy/HOL_Specific.thy Sat May 24 20:12:18 2008 +0200 +++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Sat May 24 22:04:44 2008 +0200 @@ -413,19 +413,16 @@ @{command_def (HOL) "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} @@ -492,9 +489,6 @@ may result in several theroems. Also note that this automatic transformation only works for ML-style datatype patterns. - \item [@{text "\ name"}] gives the target for the definition. - %FIXME ?!? - \item [@{text 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.