# HG changeset patch
# User wenzelm
# Date 1434218874 -7200
# Node ID 0d10ae17e3ee211ab49bea4b80cec097bc220259
# Parent  f31f7599ef55af54c7d2502cf6634647996cb07d
tuned proofs;

diff -r f31f7599ef55 -r 0d10ae17e3ee src/HOL/Hahn_Banach/Hahn_Banach_Ext_Lemmas.thy
--- a/src/HOL/Hahn_Banach/Hahn_Banach_Ext_Lemmas.thy	Sat Jun 13 19:53:53 2015 +0200
+++ b/src/HOL/Hahn_Banach/Hahn_Banach_Ext_Lemmas.thy	Sat Jun 13 20:07:54 2015 +0200
@@ -69,7 +69,8 @@
     fix y assume "y \<in> F"
     then have "a y \<in> ?S" by blast
     with xi have "a y \<le> xi" by (rule lub.upper)
-  } moreover {
+  }
+  moreover {
     fix y assume y: "y \<in> F"
     from xi have "xi \<le> b y"
     proof (rule lub.least)
@@ -78,7 +79,8 @@
       from u y have "a u \<le> b y" by (rule r)
       with au show "au \<le> b y" by (simp only:)
     qed
-  } ultimately show "\<exists>xi. \<forall>y \<in> F. a y \<le> xi \<and> xi \<le> b y" by blast
+  }
+  ultimately show "\<exists>xi. \<forall>y \<in> F. a y \<le> xi \<and> xi \<le> b y" by blast
 qed
 
 text \<open>
diff -r f31f7599ef55 -r 0d10ae17e3ee src/HOL/Hahn_Banach/Hahn_Banach_Sup_Lemmas.thy
--- a/src/HOL/Hahn_Banach/Hahn_Banach_Sup_Lemmas.thy	Sat Jun 13 19:53:53 2015 +0200
+++ b/src/HOL/Hahn_Banach/Hahn_Banach_Sup_Lemmas.thy	Sat Jun 13 20:07:54 2015 +0200
@@ -126,11 +126,11 @@
     @{text x} and @{text y} are contained in the greater
     one. \label{cases1}\<close>
 
-  from cM c'' c' have "graph H'' h'' \<subseteq> graph H' h' \<or> graph H' h' \<subseteq> graph H'' h''"
-    (is "?case1 \<or> ?case2") ..
+  from cM c'' c' consider "graph H'' h'' \<subseteq> graph H' h'" | "graph H' h' \<subseteq> graph H'' h''"
+    by (blast dest: chainsD)
   then show ?thesis
-  proof
-    assume ?case1
+  proof cases
+    case 1
     have "(x, h x) \<in> graph H'' h''" by fact
     also have "\<dots> \<subseteq> graph H' h'" by fact
     finally have xh:"(x, h x) \<in> graph H' h'" .
@@ -139,14 +139,16 @@
     moreover from cM u and c' have "graph H' h' \<subseteq> graph H h" by blast
     ultimately show ?thesis using * by blast
   next
-    assume ?case2
+    case 2
     from x_hx have "x \<in> H''" ..
-    moreover {
+    moreover have "y \<in> H''"
+    proof -
       have "(y, h y) \<in> graph H' h'" by (rule y_hy)
       also have "\<dots> \<subseteq> graph H'' h''" by fact
       finally have "(y, h y) \<in> graph H'' h''" .
-    } then have "y \<in> H''" ..
-    moreover from cM u and c'' have "graph H'' h'' \<subseteq> graph H h" by blast
+      then show ?thesis ..
+    qed
+    moreover from u c'' have "graph H'' h'' \<subseteq> graph H h" by blast
     ultimately show ?thesis using ** by blast
   qed
 qed
@@ -179,10 +181,11 @@
     or vice versa, since both @{text "G\<^sub>1"} and @{text
     "G\<^sub>2"} are members of @{text c}. \label{cases2}\<close>
 
-  from cM G1 G2 have "G1 \<subseteq> G2 \<or> G2 \<subseteq> G1" (is "?case1 \<or> ?case2") ..
+  from cM G1 G2 consider "G1 \<subseteq> G2" | "G2 \<subseteq> G1"
+    by (blast dest: chainsD)
   then show ?thesis
-  proof
-    assume ?case1
+  proof cases
+    case 1
     with xy' G2_rep have "(x, y) \<in> graph H2 h2" by blast
     then have "y = h2 x" ..
     also
@@ -190,7 +193,7 @@
     then have "z = h2 x" ..
     finally show ?thesis .
   next
-    assume ?case2
+    case 2
     with xz' G1_rep have "(x, z) \<in> graph H1 h1" by blast
     then have "z = h1 x" ..
     also