src/HOL/Library/Convex_Euclidean_Space.thy
2009-10-27 paulson 2009-10-27 New theory SupInf of the supremum and infimum operators for sets of reals.
2009-10-17 wenzelm 2009-10-17 eliminated hard tabulators, guessing at each author's individual tab-width; tuned headers;
2009-08-31 nipkow 2009-08-31 tuned the simp rules for Int involving insert and intervals.
2009-06-13 huffman 2009-06-13 generalize many constants and lemmas from Convex_Euclidean_Space
2009-06-13 huffman 2009-06-13 replace uses of (bi)linear with bounded_(bi)linear
2009-06-12 huffman 2009-06-12 replace all occurrences of dot at type real^'n with inner
2009-06-12 huffman 2009-06-12 remove simp add: norm_scaleR
2009-06-12 huffman 2009-06-12 replace all occurrences of 'op *s' at type real^'n with scaleR
2009-06-11 huffman 2009-06-11 move lemma compact_Times; generalize more lemmas
2009-06-11 huffman 2009-06-11 theorem attribute [tendsto_intros]
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