| Fri, 22 Jul 2016 11:00:43 +0200 | wenzelm | tuned proofs -- avoid unstructured calculation; | file | diff | annotate |
| Tue, 23 Feb 2016 16:25:08 +0100 | nipkow | more canonical names | file | diff | annotate |
| Thu, 10 Sep 2015 11:03:29 +0200 | nipkow | tuned | file | diff | annotate |
| Thu, 20 Mar 2014 09:47:43 +0100 | kleing | pointer to the other proof direction | file | diff | annotate |
| Thu, 26 Sep 2013 11:41:01 +0200 | nipkow | tuned | file | diff | annotate |
| Wed, 25 Sep 2013 15:49:09 +0200 | nipkow | tuned | file | diff | annotate |
| Sun, 01 Sep 2013 16:38:04 +1000 | kleing | remove redundant (simp del: ..) | file | diff | annotate |
| Thu, 08 Aug 2013 18:13:12 +0200 | kleing | avoid re-inventing transitive closure | file | diff | annotate |
| Thu, 20 Jun 2013 17:26:16 +0200 | nipkow | tuned theory name | file | diff | annotate | base |