| Fri, 22 Mar 2013 10:41:43 +0100 | hoelzl | introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it | file | diff | annotate |
| Fri, 14 Dec 2012 15:46:01 +0100 | hoelzl | Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors | file | diff | annotate |
| Wed, 10 Aug 2011 09:23:42 -0700 | huffman | split Linear_Algebra.thy from Euclidean_Space.thy | file | diff | annotate |