1.1 --- a/doc-src/IsarRef/Thy/Proof.thy	Mon Jun 07 18:09:18 2010 +0200
     1.2 +++ b/doc-src/IsarRef/Thy/Proof.thy	Mon Jun 07 19:21:00 2010 +0200
     1.3 @@ -1320,9 +1320,9 @@
     1.4    of premises of the case rule; within each premise, the \emph{prefix}
     1.5    of variables is instantiated.  In most situations, only a single
     1.6    term needs to be specified; this refers to the first variable of the
     1.7 -  last premise (it is usually the same for all cases).
     1.8 -  The \texttt{no\_simp} option can be used to disable pre-simplification
     1.9 -  of cases (see the description of @{method induct} below for details).
    1.10 +  last premise (it is usually the same for all cases).  The @{text
    1.11 +  "(no_simp)"} option can be used to disable pre-simplification of
    1.12 +  cases (see the description of @{method induct} below for details).
    1.13  
    1.14    \item @{method induct}~@{text "insts R"} is analogous to the
    1.15    @{method cases} method, but refers to induction rules, which are
    1.16 @@ -1344,28 +1344,28 @@
    1.17    present in the induction rule.  This enables the writer to specify
    1.18    only induction variables, or both predicates and variables, for
    1.19    example.
    1.20 -  
    1.21 +
    1.22    Instantiations may be definitional: equations @{text "x \<equiv> t"}
    1.23    introduce local definitions, which are inserted into the claim and
    1.24    discharged after applying the induction rule.  Equalities reappear
    1.25    in the inductive cases, but have been transformed according to the
    1.26    induction principle being involved here.  In order to achieve
    1.27    practically useful induction hypotheses, some variables occurring in
    1.28 -  @{text t} need to be fixed (see below).
    1.29 -  Instantiations of the form @{text t}, where @{text t} is not a variable,
    1.30 -  are taken as a shorthand for \mbox{@{text "x \<equiv> t"}}, where @{text x} is
    1.31 -  a fresh variable. If this is not intended, @{text t} has to be enclosed in
    1.32 -  parentheses.
    1.33 -  By default, the equalities generated by definitional instantiations
    1.34 -  are pre-simplified using a specific set of rules, usually consisting
    1.35 -  of distinctness and injectivity theorems for datatypes. This pre-simplification
    1.36 -  may cause some of the parameters of an inductive case to disappear,
    1.37 -  or may even completely delete some of the inductive cases, if one of
    1.38 -  the equalities occurring in their premises can be simplified to @{text False}.
    1.39 -  The \texttt{no\_simp} option can be used to disable pre-simplification.
    1.40 -  Additional rules to be used in pre-simplification can be declared using the
    1.41 -  \texttt{induct\_simp} attribute.
    1.42 -  
    1.43 +  @{text t} need to be fixed (see below).  Instantiations of the form
    1.44 +  @{text t}, where @{text t} is not a variable, are taken as a
    1.45 +  shorthand for \mbox{@{text "x \<equiv> t"}}, where @{text x} is a fresh
    1.46 +  variable. If this is not intended, @{text t} has to be enclosed in
    1.47 +  parentheses.  By default, the equalities generated by definitional
    1.48 +  instantiations are pre-simplified using a specific set of rules,
    1.49 +  usually consisting of distinctness and injectivity theorems for
    1.50 +  datatypes. This pre-simplification may cause some of the parameters
    1.51 +  of an inductive case to disappear, or may even completely delete
    1.52 +  some of the inductive cases, if one of the equalities occurring in
    1.53 +  their premises can be simplified to @{text False}.  The @{text
    1.54 +  "(no_simp)"} option can be used to disable pre-simplification.
    1.55 +  Additional rules to be used in pre-simplification can be declared
    1.56 +  using the @{attribute_def induct_simp} attribute.
    1.57 +
    1.58    The optional ``@{text "arbitrary: x\<^sub>1 \<dots> x\<^sub>m"}''
    1.59    specification generalizes variables @{text "x\<^sub>1, \<dots>,
    1.60    x\<^sub>m"} of the original goal before applying induction.  Thus

     2.1 --- a/doc-src/IsarRef/Thy/document/Proof.tex	Mon Jun 07 18:09:18 2010 +0200
     2.2 +++ b/doc-src/IsarRef/Thy/document/Proof.tex	Mon Jun 07 19:21:00 2010 +0200
     2.3 @@ -1317,9 +1317,8 @@
     2.4    of premises of the case rule; within each premise, the \emph{prefix}
     2.5    of variables is instantiated.  In most situations, only a single
     2.6    term needs to be specified; this refers to the first variable of the
     2.7 -  last premise (it is usually the same for all cases).
     2.8 -  The \texttt{no\_simp} option can be used to disable pre-simplification
     2.9 -  of cases (see the description of \hyperlink{method.induct}{\mbox{\isa{induct}}} below for details).
    2.10 +  last premise (it is usually the same for all cases).  The \isa{{\isachardoublequote}{\isacharparenleft}no{\isacharunderscore}simp{\isacharparenright}{\isachardoublequote}} option can be used to disable pre-simplification of
    2.11 +  cases (see the description of \hyperlink{method.induct}{\mbox{\isa{induct}}} below for details).
    2.12  
    2.13    \item \hyperlink{method.induct}{\mbox{\isa{induct}}}~\isa{{\isachardoublequote}insts\ R{\isachardoublequote}} is analogous to the
    2.14    \hyperlink{method.cases}{\mbox{\isa{cases}}} method, but refers to induction rules, which are
    2.15 @@ -1341,28 +1340,27 @@
    2.16    present in the induction rule.  This enables the writer to specify
    2.17    only induction variables, or both predicates and variables, for
    2.18    example.
    2.19 -  
    2.20 +
    2.21    Instantiations may be definitional: equations \isa{{\isachardoublequote}x\ {\isasymequiv}\ t{\isachardoublequote}}
    2.22    introduce local definitions, which are inserted into the claim and
    2.23    discharged after applying the induction rule.  Equalities reappear
    2.24    in the inductive cases, but have been transformed according to the
    2.25    induction principle being involved here.  In order to achieve
    2.26    practically useful induction hypotheses, some variables occurring in
    2.27 -  \isa{t} need to be fixed (see below).
    2.28 -  Instantiations of the form \isa{t}, where \isa{t} is not a variable,
    2.29 -  are taken as a shorthand for \mbox{\isa{{\isachardoublequote}x\ {\isasymequiv}\ t{\isachardoublequote}}}, where \isa{x} is
    2.30 -  a fresh variable. If this is not intended, \isa{t} has to be enclosed in
    2.31 -  parentheses.
    2.32 -  By default, the equalities generated by definitional instantiations
    2.33 -  are pre-simplified using a specific set of rules, usually consisting
    2.34 -  of distinctness and injectivity theorems for datatypes. This pre-simplification
    2.35 -  may cause some of the parameters of an inductive case to disappear,
    2.36 -  or may even completely delete some of the inductive cases, if one of
    2.37 -  the equalities occurring in their premises can be simplified to \isa{False}.
    2.38 -  The \texttt{no\_simp} option can be used to disable pre-simplification.
    2.39 -  Additional rules to be used in pre-simplification can be declared using the
    2.40 -  \texttt{induct\_simp} attribute.
    2.41 -  
    2.42 +  \isa{t} need to be fixed (see below).  Instantiations of the form
    2.43 +  \isa{t}, where \isa{t} is not a variable, are taken as a
    2.44 +  shorthand for \mbox{\isa{{\isachardoublequote}x\ {\isasymequiv}\ t{\isachardoublequote}}}, where \isa{x} is a fresh
    2.45 +  variable. If this is not intended, \isa{t} has to be enclosed in
    2.46 +  parentheses.  By default, the equalities generated by definitional
    2.47 +  instantiations are pre-simplified using a specific set of rules,
    2.48 +  usually consisting of distinctness and injectivity theorems for
    2.49 +  datatypes. This pre-simplification may cause some of the parameters
    2.50 +  of an inductive case to disappear, or may even completely delete
    2.51 +  some of the inductive cases, if one of the equalities occurring in
    2.52 +  their premises can be simplified to \isa{False}.  The \isa{{\isachardoublequote}{\isacharparenleft}no{\isacharunderscore}simp{\isacharparenright}{\isachardoublequote}} option can be used to disable pre-simplification.
    2.53 +  Additional rules to be used in pre-simplification can be declared
    2.54 +  using the \indexdef{}{attribute}{induct\_simp}\hypertarget{attribute.induct-simp}{\hyperlink{attribute.induct-simp}{\mbox{\isa{induct{\isacharunderscore}simp}}}} attribute.
    2.55 +
    2.56    The optional ``\isa{{\isachardoublequote}arbitrary{\isacharcolon}\ x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub m{\isachardoublequote}}''
    2.57    specification generalizes variables \isa{{\isachardoublequote}x\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ x\isactrlsub m{\isachardoublequote}} of the original goal before applying induction.  Thus
    2.58    induction hypotheses may become sufficiently general to get the