src/HOL/Library/Library.thy
changeset 31359 0c4ec2867a4e
parent 31283 86093a969bcd
child 31379 213299656575
--- a/src/HOL/Library/Library.thy	Thu May 28 22:54:57 2009 -0700
+++ b/src/HOL/Library/Library.thy	Tue Jun 02 10:00:29 2009 +0200
@@ -14,6 +14,7 @@
   Commutative_Ring
   Continuity
   ContNotDenum
+  Convex_Euclidean_Space
   Countable
   Determinants
   Diagonalize