src/HOL/Library/Convex.thy

--- a/src/HOL/Library/Convex.thy	Tue May 04 17:53:20 2010 +0200
+++ b/src/HOL/Library/Convex.thy	Tue May 04 18:05:22 2010 +0200
@@ -1,3 +1,10 @@
+(*  Title:      HOL/Library/Convex.thy
+    Author:     Armin Heller, TU Muenchen
+    Author:     Johannes Hoelzl, TU Muenchen
+*)
+
+header {* Convexity in real vector spaces *}
+
 theory Convex
 imports Product_Vector
 begin