| Thu, 25 Jul 2013 08:57:16 +0200 | factored syntactic type classes for bot and top (by Alessandro Coglio) | file | diff | annotate |
| Sat, 15 Jun 2013 17:19:23 +0200 | lifting for primitive definitions; | file | diff | annotate |
| Tue, 05 Mar 2013 10:16:15 +0100 | more lemmas about intervals | file | diff | annotate |
| Wed, 20 Feb 2013 12:04:42 +0100 | split dense into inner_dense_order and no_top/no_bot | file | diff | annotate |
| Wed, 20 Feb 2013 12:04:42 +0100 | move auxiliary lemmas from Library/Extended_Reals to HOL image | file | diff | annotate |
| Fri, 15 Feb 2013 10:52:47 +0100 | added lemma | file | diff | annotate |
| Thu, 31 Jan 2013 11:31:27 +0100 | introduce order topology | file | diff | annotate |
| Fri, 07 Dec 2012 14:28:57 +0100 | add Int_atMost | file | diff | annotate |
| Thu, 24 May 2012 17:25:53 +0200 | tuned proofs; | file | diff | annotate |
| Tue, 03 Apr 2012 15:15:00 +0200 | modernized obsolete old-style theory name with proper new-style underscore | file | diff | annotate | base |