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