changeset 44523 | d55161d67821 |
parent 44522 | 2f7e9d890efe |
child 44524 | 04ad69081646 |
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Thu Aug 25 12:43:55 2011 -0700 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Thu Aug 25 12:52:10 2011 -0700 @@ -3094,7 +3094,6 @@ subsection {* Convexity of cone hulls *} lemma convex_cone_hull: -fixes S :: "('m::euclidean_space) set" assumes "convex S" shows "convex (cone hull S)" proof-