src/HOL/Ln.thy
2012-04-01 huffman 2012-04-01 tuned proofs
2012-03-31 huffman 2012-03-31 tuned proof
2011-08-19 huffman 2011-08-19 remove some redundant simp rules
2011-08-18 huffman 2011-08-18 optimize some proofs
2011-06-09 hoelzl 2011-06-09 lemmas relating ln x and x - 1
2011-03-13 wenzelm 2011-03-13 tuned headers;
2011-01-14 wenzelm 2011-01-14 eliminated global prems; tuned proofs;
2010-12-01 nipkow 2010-12-01 moved activation of coercion inference into RealDef and declared function real a coercion. Made use of it in theory Ln.
2010-05-09 huffman 2010-05-09 avoid using real-specific versions of generic lemmas
2009-11-13 paulson 2009-11-13 A little rationalisation
2009-07-10 avigad 2009-07-10 Repaired uses of factorial.
2009-06-30 hoelzl 2009-06-30 DERIV_ln is proved in Transcendental and in Ln, use Transcendental to prove Ln.
2009-05-29 huffman 2009-05-29 generalize constants from Lim.thy to class metric_space
2009-03-04 huffman 2009-03-04 declare power_Suc [simp]; remove redundant type-specific versions of power_Suc
2009-01-28 nipkow 2009-01-28 Replaced group_ and ring_simps by algebra_simps; removed compare_rls - use algebra_simps now
2008-12-03 haftmann 2008-12-03 made repository layout more coherent with logical distribution structure; stripped some $Id$s