| Thu, 25 Aug 2011 12:43:55 -0700 | huffman | rename subset_{interior,closure} to {interior,closure}_mono; | file | diff | annotate |
| Wed, 24 Aug 2011 11:56:57 -0700 | huffman | move geometric progression lemmas from Linear_Algebra.thy to Integration.thy where they are used | file | diff | annotate |
| Tue, 23 Aug 2011 14:11:02 -0700 | huffman | declare euclidean_simps [simp] at the point they are proved; | file | diff | annotate |
| Thu, 18 Aug 2011 13:36:58 -0700 | huffman | remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas | file | diff | annotate |
| Fri, 12 Aug 2011 20:55:22 -0700 | huffman | remove redundant lemma setsum_norm in favor of norm_setsum; | file | diff | annotate |
| Fri, 12 Aug 2011 09:17:24 -0700 | huffman | make Multivariate_Analysis work with separate set type | file | diff | annotate |