Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
generalize lemma convex_cone_hull
authorhuffman
Thu, 25 Aug 2011 12:52:10 -0700
changeset 44523 d55161d67821
parent 44522 2f7e9d890efe
child 44524 04ad69081646
generalize lemma convex_cone_hull
src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy file | annotate | diff | comparison | revisions 
--- 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-
isabelle