--- 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
--- 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
--- 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