src/HOL/Library/Library.thy
changeset 33175 2083bde13ce1
parent 32479 521cc9bf2958
child 33176 d6936fd7cda8
--- 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