# 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 "\<IN> 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.