| 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 |
| Tue, 29 Aug 2017 12:05:00 +0200 | nipkow | new file | file | diff | annotate |