src/HOL/Library/Convex_Euclidean_Space.thy
2009-06-10 huffman 2009-06-10 rewrite proof of compact_convex_combinations to avoid pastecart and vec1
2009-06-09 huffman 2009-06-09 remove uses of vec1 in continuity lemmas
2009-06-09 huffman 2009-06-09 merged
2009-06-08 huffman 2009-06-08 generalize constant 'bounded' to class metric_space
2009-06-09 himmelma 2009-06-09 removed duplicate lemmas
2009-06-04 huffman 2009-06-04 generalize norm method to work over class real_normed_vector
2009-06-03 huffman 2009-06-03 generalize some constants and lemmas to class topological_space
2009-06-02 huffman 2009-06-02 merged
2009-06-02 huffman 2009-06-02 generalize more constants
2009-06-02 berghofe 2009-06-02 merged
2009-06-02 berghofe 2009-06-02 Enclosed parts of subsection in @{text ...} to make LaTeX happy.
2009-05-29 huffman 2009-05-29 generalize at function to class perfect_space
2009-05-29 huffman 2009-05-29 generalize topological notions to class metric_space; add class perfect_space
2009-05-28 huffman 2009-05-28 move dist operation to new metric_space class
2009-05-28 huffman 2009-05-28 merged
2009-05-28 huffman 2009-05-28 generalize dist function to class real_normed_vector
2009-05-28 himmelma 2009-05-28 Corrected definition of is_interval
2009-05-28 himmelma 2009-05-28 Corrected error in Convex_Euclidean_Space
2009-05-28 himmelma 2009-05-28 Added Convex_Euclidean_Space to Library.thy and Library/IsaMakefile
2009-05-28 himmelma 2009-05-28 Added Convex_Euclidean_Space.thy