1.1 --- a/doc-src/IsarRef/Thy/Proof.thy	Fri Jul 01 18:11:17 2011 +0200
     1.2 +++ b/doc-src/IsarRef/Thy/Proof.thy	Fri Jul 01 19:42:07 2011 +0200
     1.3 @@ -1366,11 +1366,12 @@
     1.4  
     1.5    The optional ``@{text "arbitrary: x\<^sub>1 \<dots> x\<^sub>m"}''
     1.6    specification generalizes variables @{text "x\<^sub>1, \<dots>,
     1.7 -  x\<^sub>m"} of the original goal before applying induction.  Thus
     1.8 -  induction hypotheses may become sufficiently general to get the
     1.9 -  proof through.  Together with definitional instantiations, one may
    1.10 -  effectively perform induction over expressions of a certain
    1.11 -  structure.
    1.12 +  x\<^sub>m"} of the original goal before applying induction.  One can
    1.13 +  separate variables by ``@{text "and"}'' to generalize them in other
    1.14 +  goals then the first. Thus induction hypotheses may become
    1.15 +  sufficiently general to get the proof through.  Together with
    1.16 +  definitional instantiations, one may effectively perform induction
    1.17 +  over expressions of a certain structure.
    1.18    
    1.19    The optional ``@{text "taking: t\<^sub>1 \<dots> t\<^sub>n"}''
    1.20    specification provides additional instantiations of a prefix of

     2.1 --- a/doc-src/IsarRef/Thy/document/Proof.tex	Fri Jul 01 18:11:17 2011 +0200
     2.2 +++ b/doc-src/IsarRef/Thy/document/Proof.tex	Fri Jul 01 19:42:07 2011 +0200
     2.3 @@ -1898,11 +1898,12 @@
     2.4    using the \indexdef{}{attribute}{induct\_simp}\hypertarget{attribute.induct-simp}{\hyperlink{attribute.induct-simp}{\mbox{\isa{induct{\isaliteral{5F}{\isacharunderscore}}simp}}}} attribute.
     2.5  
     2.6    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}}}''
     2.7 -  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
     2.8 -  induction hypotheses may become sufficiently general to get the
     2.9 -  proof through.  Together with definitional instantiations, one may
    2.10 -  effectively perform induction over expressions of a certain
    2.11 -  structure.
    2.12 +  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
    2.13 +  separate variables by ``\isa{{\isaliteral{22}{\isachardoublequote}}and{\isaliteral{22}{\isachardoublequote}}}'' to generalize them in other
    2.14 +  goals then the first. Thus induction hypotheses may become
    2.15 +  sufficiently general to get the proof through.  Together with
    2.16 +  definitional instantiations, one may effectively perform induction
    2.17 +  over expressions of a certain structure.
    2.18    
    2.19    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}}}''
    2.20    specification provides additional instantiations of a prefix of