diff -r 1fad3160d873 -r 2083bde13ce1 src/HOL/Library/Library.thy
--- a/src/HOL/Library/Library.thy	Fri Oct 23 14:33:07 2009 +0200
+++ b/src/HOL/Library/Library.thy	Fri Oct 23 13:23:18 2009 +0200
@@ -14,9 +14,7 @@
   Commutative_Ring
   Continuity
   ContNotDenum
-  Convex_Euclidean_Space
   Countable
-  Determinants
   Diagonalize
   Efficient_Nat
   Enum
@@ -54,7 +52,6 @@
   RBT
   State_Monad
   Sum_Of_Squares
-  Topology_Euclidean_Space
   Univ_Poly
   While_Combinator
   Word