hoelzl [Wed, 18 Apr 2012 14:29:21 +0200] rev 48462
replace the float datatype by a type with unique representation
hoelzl [Wed, 18 Apr 2012 14:29:20 +0200] rev 48461
add lemmas to remove real conversions when compared to power of numerals
hoelzl [Wed, 18 Apr 2012 14:29:20 +0200] rev 48460
add simp rules to rewrite comparisons of 1 and real
hoelzl [Wed, 18 Apr 2012 14:29:19 +0200] rev 48459
add lemma to equate floor and div
hoelzl [Wed, 18 Apr 2012 14:29:18 +0200] rev 48458
add powr_inj
hoelzl [Wed, 18 Apr 2012 14:29:17 +0200] rev 48457
add lemmas to rewrite powr to power
hoelzl [Wed, 18 Apr 2012 14:29:16 +0200] rev 48456
add lemmas to compare log with 0 and 1
hoelzl [Wed, 18 Apr 2012 14:29:05 +0200] rev 48455
add ceiling_diff_floor_le_1
kuncar [Thu, 19 Apr 2012 12:28:10 +0200] rev 48454
create thm names correctly
wenzelm [Thu, 19 Apr 2012 13:19:57 +0200] rev 48453
updated components according to tentative bundle;