1.1 --- a/src/HOL/IsaMakefile	Tue May 04 17:53:20 2010 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Tue May 04 18:05:22 2010 +0200
     1.3 @@ -423,7 +423,7 @@
     1.4    Library/Nat_Bijection.thy $(SRC)/Tools/float.ML			\
     1.5    $(SRC)/HOL/Tools/float_arith.ML Library/positivstellensatz.ML		\
     1.6    Library/reify_data.ML Library/reflection.ML Library/LaTeXsugar.thy	\
     1.7 -  Library/OptionalSugar.thy \
     1.8 +  Library/OptionalSugar.thy Library/Convex.thy                          \
     1.9    Library/Predicate_Compile_Quickcheck.thy Library/SML_Quickcheck.thy
    1.10  	@cd Library; $(ISABELLE_TOOL) usedir $(OUT)/HOL Library
    1.11  

     2.1 --- a/src/HOL/Library/Convex.thy	Tue May 04 17:53:20 2010 +0200
     2.2 +++ b/src/HOL/Library/Convex.thy	Tue May 04 18:05:22 2010 +0200
     2.3 @@ -1,3 +1,10 @@
     2.4 +(*  Title:      HOL/Library/Convex.thy
     2.5 +    Author:     Armin Heller, TU Muenchen
     2.6 +    Author:     Johannes Hoelzl, TU Muenchen
     2.7 +*)
     2.8 +
     2.9 +header {* Convexity in real vector spaces *}
    2.10 +
    2.11  theory Convex
    2.12  imports Product_Vector
    2.13  begin

     3.1 --- a/src/HOL/Library/Library.thy	Tue May 04 17:53:20 2010 +0200
     3.2 +++ b/src/HOL/Library/Library.thy	Tue May 04 18:05:22 2010 +0200
     3.3 @@ -12,6 +12,7 @@
     3.4    Code_Integer
     3.5    Continuity
     3.6    ContNotDenum
     3.7 +  Convex
     3.8    Countable
     3.9    Diagonalize
    3.10    Dlist