src/HOL/Library/Log_Nat.thy
20 months ago immler 2018-02-05 added lemmas, avoid 'float_of 0'
24 months ago immler 2017-10-24 generalized lemmas cancelling real_of_int/real in (in)equalities with power; completed set of related simp rules; lemmas about floorlog/bitlen
2016-08-12 nipkow 2016-08-12 tuned
2016-08-12 nipkow 2016-08-12 Extracted floorlog and bitlen to separate theory Log_Nat