| Thu, 18 Aug 2011 17:32:02 -0700 | declare euclidean_component_zero[simp] at the point it is proved | file | diff | annotate |
| Thu, 18 Aug 2011 13:36:58 -0700 | remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas | file | diff | annotate |
| Fri, 12 Aug 2011 20:55:22 -0700 | remove redundant lemma setsum_norm in favor of norm_setsum; | file | diff | annotate |
| Fri, 12 Aug 2011 09:17:24 -0700 | make Multivariate_Analysis work with separate set type | file | diff | annotate |
| Thu, 11 Aug 2011 13:05:56 -0700 | modify euclidean_space class to include basis set | file | diff | annotate |
| Wed, 10 Aug 2011 18:02:16 -0700 | avoid warnings about duplicate rules | file | diff | annotate |
| Wed, 10 Aug 2011 09:23:42 -0700 | split Linear_Algebra.thy from Euclidean_Space.thy | file | diff | annotate |