| Thu, 25 Jul 2013 08:57:16 +0200 | haftmann | factored syntactic type classes for bot and top (by Alessandro Coglio) | file | diff | annotate |
| Thu, 25 Apr 2013 11:59:21 +0200 | hoelzl | revert #916271d52466; add non-topological linear_continuum type class; show linear_continuum_topology is a perfect_space | file | diff | annotate |
| Thu, 25 Apr 2013 10:35:56 +0200 | hoelzl | renamed linear_continuum_topology to connected_linorder_topology (and mention in NEWS) | file | diff | annotate |
| Tue, 05 Mar 2013 15:43:22 +0100 | hoelzl | generalized lemmas in Extended_Real_Limits | file | diff | annotate |
| Tue, 05 Mar 2013 15:43:08 +0100 | hoelzl | move Liminf / Limsup lemmas on complete_lattices to its own file | file | diff | annotate |
| Wed, 20 Feb 2013 12:04:42 +0100 | hoelzl | split dense into inner_dense_order and no_top/no_bot | file | diff | annotate |
| Wed, 20 Feb 2013 12:04:42 +0100 | hoelzl | move auxiliary lemmas from Library/Extended_Reals to HOL image | file | diff | annotate |