1.1 --- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Thu Aug 18 12:06:17 2011 +0200
     1.2 +++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Thu Aug 18 17:00:15 2011 +0200
     1.3 @@ -157,8 +157,11 @@
     1.4    \item @{text R.cases} is the case analysis (or elimination) rule;
     1.5  
     1.6    \item @{text R.induct} or @{text R.coinduct} is the (co)induction
     1.7 -  rule.
     1.8 -
     1.9 +  rule;
    1.10 +
    1.11 +  \item @{text R.simps} is the equation unrolling the fixpoint of the
    1.12 +  predicate one step.
    1.13 + 
    1.14    \end{description}
    1.15  
    1.16    When several predicates @{text "R\<^sub>1, \<dots>, R\<^sub>n"} are

     2.1 --- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Thu Aug 18 12:06:17 2011 +0200
     2.2 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Thu Aug 18 17:00:15 2011 +0200
     2.3 @@ -225,8 +225,11 @@
     2.4    \item \isa{R{\isaliteral{2E}{\isachardot}}cases} is the case analysis (or elimination) rule;
     2.5  
     2.6    \item \isa{R{\isaliteral{2E}{\isachardot}}induct} or \isa{R{\isaliteral{2E}{\isachardot}}coinduct} is the (co)induction
     2.7 -  rule.
     2.8 -
     2.9 +  rule;
    2.10 +
    2.11 +  \item \isa{R{\isaliteral{2E}{\isachardot}}simps} is the equation unrolling the fixpoint of the
    2.12 +  predicate one step.
    2.13 + 
    2.14    \end{description}
    2.15  
    2.16    When several predicates \isa{{\isaliteral{22}{\isachardoublequote}}R\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ R\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}} are