# HG changeset patch
# User wenzelm
# Date 1135347418 -3600
# Node ID 95e6c9ef748817119a5adf4ad35521c936368e41
# Parent  6574d62fe76ba7e5be462c6eb2001eaf13cb3d8a
induct etc.: admit multiple rules;

diff -r 6574d62fe76b -r 95e6c9ef7488 doc-src/IsarRef/generic.tex
--- a/doc-src/IsarRef/generic.tex	Fri Dec 23 15:16:56 2005 +0100
+++ b/doc-src/IsarRef/generic.tex	Fri Dec 23 15:16:58 2005 +0100
@@ -1353,7 +1353,7 @@
 
   open: '(' 'open' ')'
   ;
-  rule: ('type' | 'set') ':' nameref | 'rule' ':' thmref
+  rule: ('type' | 'set') ':' (nameref +) | 'rule' ':' (thmref +)
   ;
   definst: name ('==' | equiv) term | inst
   ;
@@ -1402,13 +1402,13 @@
     \edrv x \in A   & induct & \dots         & \Text{set induction (of $A$)} \\
     \dots           & induct & \dots ~ R     & \Text{explicit rule $R$} \\
   \end{matharray}
-
-  Several instantiations may be given, each referring to some part of a mutual
-  inductive definition or datatype --- only related partial induction rules
-  may be used together, though.  Any of the lists of terms $P, x, \dots$
-  refers to the \emph{suffix} of variables present in the induction rule.
-  This enables the writer to specify only induction variables, or both
-  predicates and variables, for example.
+  
+  Several instantiations may be given, each referring to some part of
+  a mutual inductive definition or datatype --- only related partial
+  induction rules may be used together, though.  Any of the lists of
+  terms $P, x, \dots$ refers to the \emph{suffix} of variables present
+  in the induction rule.  This enables the writer to specify only
+  induction variables, or both predicates and variables, for example.
   
   Instantiations may be definitional: equations $x \equiv t$ introduce local
   definitions, which are inserted into the claim and discharged after applying