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