# HG changeset patch
# User wenzelm
# Date 1454872835 -3600
# Node ID 443256a200336884905bfd9affed5bb88c55690c
# Parent  e6669fdfe75953ab052f69b7537fd87feabbade5
more on 'consider';

diff -r e6669fdfe759 -r 443256a20033 src/Doc/Isar_Ref/Synopsis.thy
--- a/src/Doc/Isar_Ref/Synopsis.thy	Sun Feb 07 19:49:50 2016 +0100
+++ b/src/Doc/Isar_Ref/Synopsis.thy	Sun Feb 07 20:20:35 2016 +0100
@@ -313,10 +313,10 @@
 \<close>
 
 
-subsection \<open>Degenerate calculations and bigstep reasoning\<close>
+subsection \<open>Degenerate calculations\<close>
 
-text \<open>The Idea is to append \<open>this\<close> to \<open>calculation\<close>,
-  without rule composition.\<close>
+text \<open>The Idea is to append \<open>this\<close> to \<open>calculation\<close>, without rule composition.
+  This is occasionally useful to avoid naming intermediate facts.\<close>
 
 notepad
 begin
@@ -337,19 +337,11 @@
   have C \<proof>
   ultimately
   have "A \<and> B \<and> C" by blast
-next
-  txt \<open>More ambitious bigstep reasoning involving structured results:\<close>
-  have "A \<or> B \<or> C" \<proof>
-  moreover
-  { assume A have R \<proof> }
-  moreover
-  { assume B have R \<proof> }
-  moreover
-  { assume C have R \<proof> }
-  ultimately
-  have R by blast  \<comment> \<open>``big-bang integration'' of proof blocks (occasionally fragile)\<close>
 end
 
+text \<open>Note that For multi-branch case splitting, it is better to use @{command
+  consider}.\<close>
+
 
 section \<open>Induction\<close>
 
@@ -1055,6 +1047,36 @@
 end
 
 
+subsection \<open>Elimination statements and case-splitting\<close>
+
+text \<open>
+  The @{command consider} states rules for generalized elimination and case
+  splitting. This is like a toplevel statement \<^theory_text>\<open>theorem obtains\<close> used within
+  a proof body; or like a multi-branch \<^theory_text>\<open>obtain\<close> without activation of the
+  local context elements yet.
+
+  The proof method @{method cases} is able to use such rules with
+  forward-chaining (e.g.\ via \<^theory_text>\<open>then\<close>). This leads to the subsequent pattern
+  for case-splitting in a particular situation within a proof.
+\<close>
+
+notepad
+begin
+  consider (a) A | (b) B | (c) C
+    \<proof>  \<comment> \<open>typically \<^theory_text>\<open>by auto\<close>, \<^theory_text>\<open>by blast\<close> etc.\<close>
+  then have something
+  proof cases
+    case a
+    then show ?thesis \<proof>
+  next
+    case b
+    then show ?thesis \<proof>
+  next
+    case c
+    then show ?thesis \<proof>
+  qed
+end
+
 subsection \<open>Obtaining local contexts\<close>
 
 text \<open>A single ``case'' branch may be inlined into Isar proof text