src/HOL/Ln.thy
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