'fixes': support plain vars;
classical attributes: optional weight -- ignored by automated tools;

--- a/doc-src/IsarRef/generic.tex	Mon Jan 30 10:13:28 2006 +0100
+++ b/doc-src/IsarRef/generic.tex	Mon Jan 30 12:20:05 2006 +0100
@@ -124,7 +124,7 @@
   ;
   contextelem: fixes | constrains | assumes | defines | notes | includes
   ;
-  fixes: 'fixes' (name ('::' type)? structmixfix? + 'and')
+  fixes: 'fixes' ((name ('::' type)? structmixfix? | vars) + 'and')
   ;
   constrains: 'constrains' (name '::' type + 'and')
   ;
@@ -1145,7 +1145,7 @@
 \end{matharray}
 
 \begin{rail}
-  ('intro' | 'elim' | 'dest') ('!' | () | '?')
+  ('intro' | 'elim' | 'dest') ('!' | () | '?') nat?
   ;
   'rule' 'del'
   ;
@@ -1158,13 +1158,15 @@
 \item [$\isarcmd{print_claset}$] prints the collection of rules declared to
   the Classical Reasoner, which is also known as ``simpset'' internally
   \cite{isabelle-ref}.  This is a diagnostic command; $undo$ does not apply.
-
+  
 \item [$intro$, $elim$, and $dest$] declare introduction, elimination, and
   destruction rules, respectively.  By default, rules are considered as
   \emph{unsafe} (i.e.\ not applied blindly without backtracking), while a
   single ``!'' classifies as \emph{safe}.  Rule declarations marked by ``?''
-  coincide with those of Isabelle/Pure, cf.\ \S\ref{sec:pure-meth-att} (i.e.\
-  are only applied in single steps of the $rule$ method).
+  coincide with those of Isabelle/Pure, cf.\ \S\ref{sec:pure-meth-att} (i.e.\ 
+  are only applied in single steps of the $rule$ method).  The optional
+  natural number specifies an explicit weight argument, which is ignored by
+  automated tools, but determines the search order of single rule steps.
 
 \item [$rule~del$] deletes introduction, elimination, or destruction rules from
   the context.