| Tue, 05 Nov 2013 09:45:02 +0100 | hoelzl | move Lubs from HOL to HOL-Library (replaced by conditionally complete lattices) | file | diff | annotate |
| Tue, 05 Nov 2013 09:44:58 +0100 | hoelzl | use bdd_above and bdd_below for conditionally complete lattices | file | diff | annotate |
| Fri, 01 Nov 2013 18:51:14 +0100 | haftmann | more simplification rules on unary and binary minus | file | diff | annotate |
| Tue, 24 Sep 2013 16:03:00 +0200 | wenzelm | tuned proofs; | file | diff | annotate |
| Sat, 14 Sep 2013 22:30:10 +0200 | wenzelm | tuned proofs; | file | diff | annotate |
| Sat, 14 Sep 2013 13:59:57 +0200 | wenzelm | tuned proofs; | file | diff | annotate |
| Thu, 12 Sep 2013 18:09:17 -0700 | huffman | make 'linear' into a sublocale of 'bounded_linear'; | file | diff | annotate |