# HG changeset patch
# User wenzelm
# Date 1211659488 -7200
# Node ID 978cefd606ad3e89ca88dcc998c3ac641c59e01b
# Parent  0736fa14c275886474fdcf98854bc8c1c15ea95f
updated generated file;

diff -r 0736fa14c275 -r 978cefd606ad doc-src/IsarRef/Thy/document/HOL_Specific.tex
--- 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.
diff -r 0736fa14c275 -r 978cefd606ad doc-src/IsarRef/Thy/document/intro.tex
--- a/doc-src/IsarRef/Thy/document/intro.tex	Sat May 24 22:04:46 2008 +0200
+++ b/doc-src/IsarRef/Thy/document/intro.tex	Sat May 24 22:04:48 2008 +0200
@@ -92,8 +92,8 @@
 Isar is already part of Isabelle.  The low-level \verb|isabelle| binary provides option \verb|-I| to run the
   Isabelle/Isar interaction loop at startup, rather than the raw ML
   top-level.  So the most basic way to do anything with Isabelle/Isar
-  is as follows:
-\begin{ttbox}  % FIXME update
+  is as follows:   % FIXME update
+\begin{ttbox}
 isabelle -I HOL\medskip
 \out{> Welcome to Isabelle/HOL (Isabelle2005)}\medskip
 theory Foo imports Main begin;