| Thu, 28 May 2009 13:41:41 -0700 | huffman | generalize dist function to class real_normed_vector | changeset | files |
| Thu, 28 May 2009 20:01:38 +0200 | bulwahn | added remark to code | changeset | files |
| Thu, 28 May 2009 18:59:51 +0200 | himmelma | Removed Convex_Euclidean_Space.thy from Library. | changeset | files |