src/HOL/Library/Log_Nat.thy
22 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