| Sun, 09 May 2010 17:47:43 -0700 | huffman | avoid using real-specific versions of generic lemmas | file | diff | annotate |
| Fri, 13 Nov 2009 17:15:12 +0000 | paulson | A little rationalisation | file | diff | annotate |
| Fri, 10 Jul 2009 12:55:06 -0400 | avigad | Repaired uses of factorial. | file | diff | annotate |
| Tue, 30 Jun 2009 18:25:55 +0200 | hoelzl | DERIV_ln is proved in Transcendental and in Ln, use Transcendental to prove Ln. | file | diff | annotate |
| Fri, 29 May 2009 09:22:56 -0700 | huffman | generalize constants from Lim.thy to class metric_space | file | diff | annotate |
| Wed, 04 Mar 2009 17:12:23 -0800 | huffman | declare power_Suc [simp]; remove redundant type-specific versions of power_Suc | file | diff | annotate |
| Wed, 28 Jan 2009 16:29:16 +0100 | nipkow | Replaced group_ and ring_simps by algebra_simps; | file | diff | annotate |
| Wed, 03 Dec 2008 15:58:44 +0100 | haftmann | made repository layout more coherent with logical distribution structure; stripped some $Id$s | file | diff | annotate | base |