diff -r 08d227db6c74 -r 503ac4c5ef91 doc-src/IsarRef/generic.tex
--- a/doc-src/IsarRef/generic.tex	Mon Sep 11 14:35:30 2006 +0200
+++ b/doc-src/IsarRef/generic.tex	Mon Sep 11 21:35:19 2006 +0200
@@ -1516,7 +1516,7 @@
 \begin{rail}
   'cases' open? (insts * 'and') rule?
   ;
-  'induct' open? (definsts * 'and') \\ fixing? taking? rule?
+  'induct' open? (definsts * 'and') \\ arbitrary? taking? rule?
   ;
   'coinduct' open? insts taking rule?
   ;
@@ -1529,7 +1529,7 @@
   ;
   definsts: ( definst *)
   ;
-  fixing: 'fixing' ':' ((term *) 'and' +)
+  arbitrary: 'arbitrary' ':' ((term *) 'and' +)
   ;
   taking: 'taking' ':' insts
   ;
@@ -1587,11 +1587,11 @@
   In order to achieve practically useful induction hypotheses, some variables
   occurring in $t$ need to be fixed (see below).
   
-  The optional ``$fixing\colon \vec x$'' specification generalizes variables
-  $\vec x$ of the original goal before applying induction.  Thus induction
-  hypotheses may become sufficiently general to get the proof through.
-  Together with definitional instantiations, one may effectively perform
-  induction over expressions of a certain structure.
+  The optional ``$arbitrary\colon \vec x$'' specification generalizes
+  variables $\vec x$ of the original goal before applying induction.  Thus
+  induction hypotheses may become sufficiently general to get the proof
+  through.  Together with definitional instantiations, one may effectively
+  perform induction over expressions of a certain structure.
   
   The optional ``$taking\colon \vec t$'' specification provides additional
   instantiations of a prefix of pending variables in the rule.  Such schematic