# HG changeset patch
# User wenzelm
# Date 1433927686 -7200
# Node ID 285c7ff27728668255a2b1e5693b15ed55b4ddb4
# Parent  8f7e1279251d12ce5bbb3f075f9a25356ed4433e
tuned proofs;

diff -r 8f7e1279251d -r 285c7ff27728 src/HOL/Hahn_Banach/Hahn_Banach_Sup_Lemmas.thy
--- 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])
diff -r 8f7e1279251d -r 285c7ff27728 src/HOL/Hahn_Banach/Subspace.thy
--- 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