| Fri, 29 May 2009 22:42:13 -0700 | huffman | generalize at function to class perfect_space | file | diff | annotate |
| Fri, 29 May 2009 18:23:07 -0700 | huffman | generalize topological notions to class metric_space; add class perfect_space | file | diff | annotate |
| Thu, 28 May 2009 17:00:02 -0700 | huffman | move dist operation to new metric_space class | file | diff | annotate |
| Thu, 28 May 2009 13:43:45 -0700 | huffman | merged | file | diff | annotate |
| Thu, 28 May 2009 13:41:41 -0700 | huffman | generalize dist function to class real_normed_vector | file | diff | annotate |
| Thu, 28 May 2009 16:19:34 +0200 | himmelma | Corrected definition of is_interval | file | diff | annotate |
| Thu, 28 May 2009 15:42:44 +0200 | himmelma | Corrected error in Convex_Euclidean_Space | file | diff | annotate |
| Thu, 28 May 2009 13:56:50 +0200 | himmelma | Added Convex_Euclidean_Space to Library.thy and Library/IsaMakefile | file | diff | annotate |
| Thu, 28 May 2009 09:46:45 +0200 | himmelma | Added Convex_Euclidean_Space.thy | file | diff | annotate |