# HG changeset patch
# User hoelzl
# Date 1272989122 -7200
# Node ID 43b66dcd926603da09317838590a9c18bb94093d
# Parent  edc381bf72006af2a21395fa2d9be749695cdacc
Add Convex to Library build

diff -r edc381bf7200 -r 43b66dcd9266 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Tue May 04 17:53:20 2010 +0200
+++ b/src/HOL/IsaMakefile	Tue May 04 18:05:22 2010 +0200
@@ -423,7 +423,7 @@
   Library/Nat_Bijection.thy $(SRC)/Tools/float.ML			\
   $(SRC)/HOL/Tools/float_arith.ML Library/positivstellensatz.ML		\
   Library/reify_data.ML Library/reflection.ML Library/LaTeXsugar.thy	\
-  Library/OptionalSugar.thy \
+  Library/OptionalSugar.thy Library/Convex.thy                          \
   Library/Predicate_Compile_Quickcheck.thy Library/SML_Quickcheck.thy
 	@cd Library; $(ISABELLE_TOOL) usedir $(OUT)/HOL Library
 
diff -r edc381bf7200 -r 43b66dcd9266 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
diff -r edc381bf7200 -r 43b66dcd9266 src/HOL/Library/Library.thy
--- a/src/HOL/Library/Library.thy	Tue May 04 17:53:20 2010 +0200
+++ b/src/HOL/Library/Library.thy	Tue May 04 18:05:22 2010 +0200
@@ -12,6 +12,7 @@
   Code_Integer
   Continuity
   ContNotDenum
+  Convex
   Countable
   Diagonalize
   Dlist