src/HOL/Hahn_Banach/Hahn_Banach_Ext_Lemmas.thy

--- a/src/HOL/Hahn_Banach/Hahn_Banach_Ext_Lemmas.thy	Sun Apr 24 21:31:14 2016 +0200
+++ b/src/HOL/Hahn_Banach/Hahn_Banach_Ext_Lemmas.thy	Mon Apr 25 16:09:26 2016 +0200
@@ -86,9 +86,9 @@
 \<close>
 
 lemma h'_lf:
-  assumes h'_def: "h' \<equiv> \<lambda>x. let (y, a) =
-      SOME (y, a). x = y + a \<cdot> x0 \<and> y \<in> H in h y + a * xi"
-    and H'_def: "H' \<equiv> H + lin x0"
+  assumes h'_def: "\<And>x. h' x = (let (y, a) =
+      SOME (y, a). x = y + a \<cdot> x0 \<and> y \<in> H in h y + a * xi)"
+    and H'_def: "H' = H + lin x0"
     and HE: "H \<unlhd> E"
   assumes "linearform H h"
   assumes x0: "x0 \<notin> H"  "x0 \<in> E"  "x0 \<noteq> 0"
@@ -192,9 +192,9 @@
 \<close>
 
 lemma h'_norm_pres:
-  assumes h'_def: "h' \<equiv> \<lambda>x. let (y, a) =
-      SOME (y, a). x = y + a \<cdot> x0 \<and> y \<in> H in h y + a * xi"
-    and H'_def: "H' \<equiv> H + lin x0"
+  assumes h'_def: "\<And>x. h' x = (let (y, a) =
+      SOME (y, a). x = y + a \<cdot> x0 \<and> y \<in> H in h y + a * xi)"
+    and H'_def: "H' = H + lin x0"
     and x0: "x0 \<notin> H"  "x0 \<in> E"  "x0 \<noteq> 0"
   assumes E: "vectorspace E" and HE: "subspace H E"
     and "seminorm E p" and "linearform H h"