| Tue, 24 Oct 2017 18:48:21 +0200 | immler | generalized lemmas cancelling real_of_int/real in (in)equalities with power; completed set of related simp rules; lemmas about floorlog/bitlen | file | diff | annotate |
| Fri, 12 Aug 2016 09:57:09 +0200 | nipkow | tuned | file | diff | annotate |
| Fri, 12 Aug 2016 08:20:17 +0200 | nipkow | Extracted floorlog and bitlen to separate theory Log_Nat | file | diff | annotate |