# HG changeset patch
# User haftmann
# Date 1313700628 -7200
# Node ID d27b9fe4759e8bc08a35e1d94086d86d5a52f4a8
# Parent  d995733b635df12acc85729801ac546a9f52b45f# Parent  4846f3f320d9fbd90c354b474e2e1a74268367d3
merged

diff -r 4846f3f320d9 -r d27b9fe4759e NEWS
--- a/NEWS	Thu Aug 18 22:50:17 2011 +0200
+++ b/NEWS	Thu Aug 18 22:50:28 2011 +0200
@@ -57,6 +57,9 @@
 * Isabelle/Isar reference manual provides more formal references in
 syntax diagrams.
 
+* Attribute case_names has been refined: the assumptions in each case can
+be named now by following the case name with [name1 name2 ...].
+
 
 *** HOL ***
 
diff -r 4846f3f320d9 -r d27b9fe4759e doc-src/IsarRef/Thy/HOL_Specific.thy
--- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Thu Aug 18 22:50:17 2011 +0200
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Thu Aug 18 22:50:28 2011 +0200
@@ -157,8 +157,11 @@
   \item @{text R.cases} is the case analysis (or elimination) rule;
 
   \item @{text R.induct} or @{text R.coinduct} is the (co)induction
-  rule.
-
+  rule;
+
+  \item @{text R.simps} is the equation unrolling the fixpoint of the
+  predicate one step.
+ 
   \end{description}
 
   When several predicates @{text "R\<^sub>1, \<dots>, R\<^sub>n"} are
diff -r 4846f3f320d9 -r d27b9fe4759e doc-src/IsarRef/Thy/document/HOL_Specific.tex
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Thu Aug 18 22:50:17 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Thu Aug 18 22:50:28 2011 +0200
@@ -225,8 +225,11 @@
   \item \isa{R{\isaliteral{2E}{\isachardot}}cases} is the case analysis (or elimination) rule;
 
   \item \isa{R{\isaliteral{2E}{\isachardot}}induct} or \isa{R{\isaliteral{2E}{\isachardot}}coinduct} is the (co)induction
-  rule.
-
+  rule;
+
+  \item \isa{R{\isaliteral{2E}{\isachardot}}simps} is the equation unrolling the fixpoint of the
+  predicate one step.
+ 
   \end{description}
 
   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