isabelle: File revisions

src/HOL/Ln.thy

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

isabelle