author wenzelm Wed, 10 Jun 2015 11:14:46 +0200 changeset 60412 285c7ff27728 parent 60411 8f7e1279251d child 60413 0824fd1e9c40
tuned proofs;
```--- a/src/HOL/Hahn_Banach/Hahn_Banach_Sup_Lemmas.thy	Wed Jun 10 11:14:04 2015 +0200
+++ b/src/HOL/Hahn_Banach/Hahn_Banach_Sup_Lemmas.thy	Wed Jun 10 11:14:46 2015 +0200
@@ -420,7 +420,7 @@
show ?L
proof
fix x assume x: "x \<in> H"
-      show "\<And>a b :: real. - a \<le> b \<Longrightarrow> b \<le> a \<Longrightarrow> \<bar>b\<bar> \<le> a"
+      show "- a \<le> b \<Longrightarrow> b \<le> a \<Longrightarrow> \<bar>b\<bar> \<le> a" for a b :: real
by arith
from \<open>linearform H h\<close> and H x
have "- h x = h (- x)" by (rule linearform.neg [symmetric])```
```--- a/src/HOL/Hahn_Banach/Subspace.thy	Wed Jun 10 11:14:04 2015 +0200
+++ b/src/HOL/Hahn_Banach/Subspace.thy	Wed Jun 10 11:14:46 2015 +0200
@@ -132,7 +132,7 @@
qed
fix x y assume x: "x \<in> U" and y: "y \<in> U"
from uv and x y show "x + y \<in> U" by (rule subspace.add_closed)
-  from uv and x show "\<And>a. a \<cdot> x \<in> U" by (rule subspace.mult_closed)
+  from uv and x show "a \<cdot> x \<in> U" for a by (rule subspace.mult_closed)
qed

@@ -152,8 +152,10 @@
lemma linI' [iff]: "a \<cdot> x \<in> lin x"
unfolding lin_def by blast

-lemma linE [elim]: "x \<in> lin v \<Longrightarrow> (\<And>a::real. x = a \<cdot> v \<Longrightarrow> C) \<Longrightarrow> C"
-  unfolding lin_def by blast
+lemma linE [elim]:
+  assumes "x \<in> lin v"
+  obtains a :: real where "x = a \<cdot> v"
+  using assms unfolding lin_def by blast

text \<open>Every vector is contained in its linear closure.\<close>
@@ -263,7 +265,7 @@
qed
fix x y assume x: "x \<in> U" and "y \<in> U"
then show "x + y \<in> U" by simp
-    from x show "\<And>a. a \<cdot> x \<in> U" by simp
+    from x show "a \<cdot> x \<in> U" for a by simp
qed
qed
```