src/HOL/Ln.thy
Mon, 03 Dec 2012 18:19:05 +0100 hoelzl add filterlim rules for exp and ln to infinity
Sun, 01 Apr 2012 09:12:03 +0200 huffman tuned proofs
Sat, 31 Mar 2012 20:09:24 +0200 huffman tuned proof
Fri, 19 Aug 2011 07:45:22 -0700 huffman remove some redundant simp rules
Thu, 18 Aug 2011 19:53:03 -0700 huffman optimize some proofs
Thu, 09 Jun 2011 11:50:16 +0200 hoelzl lemmas relating ln x and x - 1
Sun, 13 Mar 2011 22:55:50 +0100 wenzelm tuned headers;
Fri, 14 Jan 2011 15:44:47 +0100 wenzelm eliminated global prems;
Wed, 01 Dec 2010 20:59:29 +0100 nipkow moved activation of coercion inference into RealDef and declared function real a coercion.
Sun, 09 May 2010 17:47:43 -0700 huffman avoid using real-specific versions of generic lemmas
Fri, 13 Nov 2009 17:15:12 +0000 paulson A little rationalisation
Fri, 10 Jul 2009 12:55:06 -0400 avigad Repaired uses of factorial.
Tue, 30 Jun 2009 18:25:55 +0200 hoelzl DERIV_ln is proved in Transcendental and in Ln, use Transcendental to prove Ln.
Fri, 29 May 2009 09:22:56 -0700 huffman generalize constants from Lim.thy to class metric_space
Wed, 04 Mar 2009 17:12:23 -0800 huffman declare power_Suc [simp]; remove redundant type-specific versions of power_Suc
Wed, 28 Jan 2009 16:29:16 +0100 nipkow Replaced group_ and ring_simps by algebra_simps;
Wed, 03 Dec 2008 15:58:44 +0100 haftmann made repository layout more coherent with logical distribution structure; stripped some $Id$s
less more (0) tip