# HG changeset patch
# User huffman
# Date 1314301930 25200
# Node ID d55161d6782188b283cfb1eeae26265ab5d2af8f
# Parent  2f7e9d890efed96a59ee0a8c12a9ba95ab305a66
generalize lemma convex_cone_hull

diff -r 2f7e9d890efe -r d55161d67821 src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
--- 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-