# HG changeset patch
# User wenzelm
# Date 936214136 -7200
# Node ID 83e60a678c3a70b04248fbf38b2ef103391b94b1
# Parent  6ea8cbf94118ef39ebb1a540bca55cf5af9a815a
fix: vars;

diff -r 6ea8cbf94118 -r 83e60a678c3a doc-src/IsarRef/pure.tex
--- a/doc-src/IsarRef/pure.tex	Wed Sep 01 21:28:42 1999 +0200
+++ b/doc-src/IsarRef/pure.tex	Wed Sep 01 21:28:56 1999 +0200
@@ -341,9 +341,10 @@
   Furthermore, the file name is checked with the $\isarkeyword{files}$
   dependency declaration given in the theory header (see also
   \S\ref{sec:begin-thy}).
+
 \item [$\isarkeyword{ML}~text$] reads and executes ML commands from $text$.
   The theory context is passed just as for $\isarkeyword{use}$.
-%FIXME picked up again!?
+
 \item [$\isarkeyword{setup}~text$] changes the current theory context by
   applying setup functions $text$, which has to be an ML expression of type
   $(theory \to theory)~list$.  The $\isarkeyword{setup}$ command is the usual
@@ -468,7 +469,7 @@
 exporting some result $\phi[x]$ simply yields $\phi[t]$.
 
 \begin{rail}
-  'fix' (var +) comment?
+  'fix' (vars + 'and') comment?
   ;
   ('assume' | 'presume') (assm comment? + 'and')
   ;
@@ -477,6 +478,8 @@
 
   var: name ('::' type)?
   ;
+  vars: name+ ('::' type)?
+  ;
   assm: thmdecl? (prop proppat? +)
   ;
 \end{rail}
@@ -496,6 +499,8 @@
   In results exported from the context, $x$ is replaced by $t$.  Basically,
   $\DEF{}{x \equiv t}$ abbreviates $\FIX{x}~\PRESUME{}{x \equiv t}$, with the
   resulting hypothetical equation solved by reflexivity.
+  
+  The default name for the definitional equation is $x_def$.
 \end{descr}
 
 The special theorem name $prems$\indexisarthm{prems} refers to all current