# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1426868300 0
# Node ID 9c99e5f9fb5e7050d0c22322ea33f40292fd4530
# Parent  26d1c71784f12075a66a913f529768d4eed3acb8# Parent  4ebf2276f58aab757ec22dc1aea57e62070ae7d9
Merge

diff -r 4ebf2276f58a -r 9c99e5f9fb5e src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy
--- a/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Fri Mar 20 16:18:28 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Fri Mar 20 16:18:20 2015 +0000
@@ -1913,14 +1913,8 @@
     using brouwer_cube by auto
   then show ?thesis
     unfolding homeomorphic_fixpoint_property[OF *]
-    apply (erule_tac x=f in allE)
-    apply (erule impE)
-    defer
-    apply (erule bexE)
-    apply (rule_tac x=y in that)
     using assms
-    apply auto
-    done
+    by (auto simp: intro: that)
 qed
 
 
@@ -1964,7 +1958,6 @@
     apply (rule continuous_on_closest_point[OF assms(2) compact_imp_closed[OF assms(1)] assms(3)])
     apply (rule continuous_on_subset[OF assms(4)])
     apply (insert closest_point_in_set[OF compact_imp_closed[OF assms(1)] assms(3)])
-    defer
     using assms(5)[unfolded subset_eq]
     using e(2)[unfolded subset_eq mem_cball]
     apply (auto simp add: dist_norm)
@@ -2002,21 +1995,10 @@
       "x \<in> {x. norm (a - x) = e}"
       "2 *\<^sub>R a - x = x"
     apply (rule retract_fixpoint_property[OF goal1, of "\<lambda>x. scaleR 2 a - x"])
-    apply rule
-    apply rule
-    apply (erule conjE)
-    apply (rule brouwer_ball[OF assms])
-    apply assumption+
-    apply (rule_tac x=x in bexI)
-    apply assumption+
-    apply (rule continuous_intros)+
-    unfolding frontier_cball subset_eq Ball_def image_iff
-    apply rule
-    apply rule
-    apply (erule bexE)
-    unfolding dist_norm
-    apply (simp add: * norm_minus_commute)
-    apply blast
+    apply (blast intro: brouwer_ball[OF assms])
+    apply (intro continuous_intros)
+    unfolding frontier_cball subset_eq Ball_def image_iff dist_norm
+    apply (auto simp add: * norm_minus_commute)
     done
   then have "scaleR 2 a = scaleR 1 x + scaleR 1 x"
     by (auto simp add: algebra_simps)
diff -r 4ebf2276f58a -r 9c99e5f9fb5e src/HOL/Multivariate_Analysis/Integration.thy
--- a/src/HOL/Multivariate_Analysis/Integration.thy	Fri Mar 20 16:18:28 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Integration.thy	Fri Mar 20 16:18:20 2015 +0000
@@ -1466,7 +1466,7 @@
       using division_ofD[OF p] by auto
     show "\<exists>p. p division_of \<Union>insert x F"
       using elementary_union_interval[OF p[unfolded *], of a b]
-      unfolding Union_insert x * by auto
+      unfolding Union_insert x * by metis
   qed (insert assms, auto)
   then show ?thesis
     apply -
@@ -4662,7 +4662,7 @@
           apply auto
           done
         ultimately show "u\<bullet>j = a\<bullet>j \<and> v\<bullet>j = a\<bullet>j \<or> u\<bullet>j = b\<bullet>j \<and> v\<bullet>j = b\<bullet>j \<or> u\<bullet>j = a\<bullet>j \<and> v\<bullet>j = b\<bullet>j"
-          unfolding not_less de_Morgan_disj using ab[rule_format,of j] uv(2) j by auto
+          unfolding not_less de_Morgan_disj using ab[rule_format,of j] uv(2) j by force
       qed
       have "(1/2) *\<^sub>R (a+b) \<in> cbox a b"
         unfolding mem_box using ab by(auto intro!: less_imp_le simp: inner_simps)
diff -r 4ebf2276f58a -r 9c99e5f9fb5e src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Fri Mar 20 16:18:28 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Fri Mar 20 16:18:20 2015 +0000
@@ -1250,7 +1250,7 @@
       e1 \<noteq> {} \<and>
       e2 \<noteq> {})"
   unfolding connected_def openin_open
-  by blast
+  by safe blast+
 
 lemma exists_diff:
   fixes P :: "'a set \<Rightarrow> bool"