--- a/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy Fri Mar 20 14:06:15 2015 +0000
+++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy Fri Mar 20 16:11:28 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)
--- a/src/HOL/Multivariate_Analysis/Integration.thy Fri Mar 20 14:06:15 2015 +0000
+++ b/src/HOL/Multivariate_Analysis/Integration.thy Fri Mar 20 16:11:28 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)
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Fri Mar 20 14:06:15 2015 +0000
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Fri Mar 20 16:11:28 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"