# HG changeset patch
# User haftmann
# Date 1309553285 -7200
# Node ID 5967e25c74664072a409405241e0389d7c33d427
# Parent  e8ee3641754e7e1633ffd3e4c9f5c5ac3f791783# Parent  93cd6dd1a1c6472fb35be15ce09f223a7a2b4015
merged

diff -r 93cd6dd1a1c6 -r 5967e25c7466 doc-src/IsarRef/Thy/Proof.thy
--- a/doc-src/IsarRef/Thy/Proof.thy	Fri Jul 01 19:57:41 2011 +0200
+++ b/doc-src/IsarRef/Thy/Proof.thy	Fri Jul 01 22:48:05 2011 +0200
@@ -1366,11 +1366,12 @@
 
   The optional ``@{text "arbitrary: x\<^sub>1 \<dots> x\<^sub>m"}''
   specification generalizes variables @{text "x\<^sub>1, \<dots>,
-  x\<^sub>m"} 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.
+  x\<^sub>m"} of the original goal before applying induction.  One can
+  separate variables by ``@{text "and"}'' to generalize them in other
+  goals then the first. 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 ``@{text "taking: t\<^sub>1 \<dots> t\<^sub>n"}''
   specification provides additional instantiations of a prefix of
diff -r 93cd6dd1a1c6 -r 5967e25c7466 doc-src/IsarRef/Thy/document/Proof.tex
--- a/doc-src/IsarRef/Thy/document/Proof.tex	Fri Jul 01 19:57:41 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/Proof.tex	Fri Jul 01 22:48:05 2011 +0200
@@ -1898,11 +1898,12 @@
   using the \indexdef{}{attribute}{induct\_simp}\hypertarget{attribute.induct-simp}{\hyperlink{attribute.induct-simp}{\mbox{\isa{induct{\isaliteral{5F}{\isacharunderscore}}simp}}}} attribute.
 
   The optional ``\isa{{\isaliteral{22}{\isachardoublequote}}arbitrary{\isaliteral{3A}{\isacharcolon}}\ x\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ x\isaliteral{5C3C5E7375623E}{}\isactrlsub m{\isaliteral{22}{\isachardoublequote}}}''
-  specification generalizes variables \isa{{\isaliteral{22}{\isachardoublequote}}x\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ x\isaliteral{5C3C5E7375623E}{}\isactrlsub m{\isaliteral{22}{\isachardoublequote}}} 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.
+  specification generalizes variables \isa{{\isaliteral{22}{\isachardoublequote}}x\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ x\isaliteral{5C3C5E7375623E}{}\isactrlsub m{\isaliteral{22}{\isachardoublequote}}} of the original goal before applying induction.  One can
+  separate variables by ``\isa{{\isaliteral{22}{\isachardoublequote}}and{\isaliteral{22}{\isachardoublequote}}}'' to generalize them in other
+  goals then the first. 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 ``\isa{{\isaliteral{22}{\isachardoublequote}}taking{\isaliteral{3A}{\isacharcolon}}\ t\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ t\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}}''
   specification provides additional instantiations of a prefix of