| Tue, 17 May 2022 14:10:14 +0100 | paulson | tidied auto / simp with null arguments | file | diff | annotate |
| Fri, 14 Jun 2019 08:34:28 +0000 | haftmann | moved some theorems into HOL main corpus | file | diff | annotate |
| Fri, 14 Jun 2019 08:34:28 +0000 | haftmann | misc tuning and modernization | file | diff | annotate |
| Thu, 07 Jun 2018 19:36:12 +0200 | nipkow | utilize 'flip' | file | diff | annotate |
| Mon, 05 Feb 2018 08:30:19 +0100 | immler | added lemmas, avoid 'float_of 0' | file | diff | annotate |
| 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 |