13 months ago nipkow 2018-06-07 utilize 'flip'
17 months ago immler 2018-02-05 added lemmas, avoid 'float_of 0'
21 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