src/HOL/Library/Library.thy
changeset 31278 60a53b5af39c
parent 31186 b458b4ac570f
child 31283 86093a969bcd
     1.1 --- a/src/HOL/Library/Library.thy	Thu May 28 09:56:04 2009 +0200
     1.2 +++ b/src/HOL/Library/Library.thy	Thu May 28 13:56:50 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