| Fri, 04 Jul 2014 20:18:47 +0200 | haftmann | reduced name variants for assoc and commute on plus and mult | file | diff | annotate |
| Fri, 28 Mar 2014 18:21:20 -0700 | huffman | minimized imports | file | diff | annotate |
| Wed, 19 Mar 2014 20:50:24 -0700 | huffman | generalize theory of operator norms to work with class real_normed_vector | file | diff | annotate |
| Tue, 05 Nov 2013 09:45:02 +0100 | hoelzl | move Lubs from HOL to HOL-Library (replaced by conditionally complete lattices) | file | diff | annotate |
| Wed, 18 Sep 2013 00:11:15 +0200 | wenzelm | tuned proofs; | file | diff | annotate |
| Wed, 28 Aug 2013 23:41:21 +0200 | wenzelm | tuned proofs; | file | diff | annotate |
| 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 |