1.1 --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Thu Dec 02 21:23:56 2010 +0100
     1.2 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Fri Dec 03 00:36:01 2010 +0100
     1.3 @@ -313,7 +313,7 @@
     1.4  
     1.5  lemma snd_linear: "linear snd" unfolding linear_def by (simp add: algebra_simps)
     1.6  
     1.7 -lemma fst_snd_linear: "linear (%z. fst z + snd z)" unfolding linear_def by (simp add: algebra_simps)
     1.8 +lemma fst_snd_linear: "linear (%(x,y). x + y)" unfolding linear_def by (simp add: algebra_simps)
     1.9  
    1.10  lemma scaleR_2:
    1.11    fixes x :: "'a::real_vector"
    1.12 @@ -5451,11 +5451,11 @@
    1.13  shows "convex hull (S \<oplus> T) = (convex hull S) \<oplus> (convex hull T)"
    1.14  proof-
    1.15  have "(convex hull S) \<oplus> (convex hull T) =
    1.16 -      (%z. fst z + snd z) ` ((convex hull S) <*> (convex hull T))"
    1.17 +      (%(x,y). x + y) ` ((convex hull S) <*> (convex hull T))"
    1.18     by (simp add: set_plus_image)
    1.19 -also have "... = (%z. fst z + snd z) ` (convex hull (S <*> T))" using convex_hull_direct_sum by auto
    1.20 +also have "... = (%(x,y). x + y) ` (convex hull (S <*> T))" using convex_hull_direct_sum by auto
    1.21  also have "...= convex hull (S \<oplus> T)" using fst_snd_linear linear_conv_bounded_linear
    1.22 -   convex_hull_linear_image[of "(%z. fst z + snd z)" "S <*> T"] by (auto simp add: set_plus_image)
    1.23 +   convex_hull_linear_image[of "(%(x,y). x + y)" "S <*> T"] by (auto simp add: set_plus_image)
    1.24  finally show ?thesis by auto
    1.25  qed
    1.26  
    1.27 @@ -5464,11 +5464,11 @@
    1.28  assumes "convex S" "convex T"
    1.29  shows "rel_interior (S \<oplus> T) = (rel_interior S) \<oplus> (rel_interior T)"
    1.30  proof-
    1.31 -have "(rel_interior S) \<oplus> (rel_interior T) = (%z. fst z + snd z) ` (rel_interior S <*> rel_interior T)"
    1.32 +have "(rel_interior S) \<oplus> (rel_interior T) = (%(x,y). x + y) ` (rel_interior S <*> rel_interior T)"
    1.33     by (simp add: set_plus_image)
    1.34 -also have "... = (%z. fst z + snd z) ` rel_interior (S <*> T)" using rel_interior_direct_sum assms by auto
    1.35 +also have "... = (%(x,y). x + y) ` rel_interior (S <*> T)" using rel_interior_direct_sum assms by auto
    1.36  also have "...= rel_interior (S \<oplus> T)" using fst_snd_linear convex_direct_sum assms
    1.37 -   rel_interior_convex_linear_image[of "(%z. fst z + snd z)" "S <*> T"] by (auto simp add: set_plus_image)
    1.38 +   rel_interior_convex_linear_image[of "(%(x,y). x + y)" "S <*> T"] by (auto simp add: set_plus_image)
    1.39  finally show ?thesis by auto
    1.40  qed
    1.41