| Wed, 13 Nov 2024 15:00:17 +0000 |
paulson |
The ceillog2 function (thanks to Manuel Eberl), replacing two copies of Ceil_Log2
|
file |
diff |
annotate
|
| Fri, 09 Aug 2024 20:45:31 +0100 |
paulson |
revised/generalised some lemmas
|
file |
diff |
annotate
|
| 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
|