| Tue, 06 Feb 2024 18:08:43 +0000 | haftmann | more lemmas and more correct lemma names | file | diff | annotate |
| Mon, 29 Jan 2024 20:37:03 +0000 | haftmann | strengthened class parity | file | diff | annotate |
| Thu, 25 Jan 2024 11:19:03 +0000 | haftmann | rearranged and reformulated abstract classes for bit structures and operations | file | diff | annotate |
| Sat, 02 Dec 2023 20:49:50 +0000 | haftmann | compactified specification of type class parity | file | diff | annotate |
| Sat, 02 Dec 2023 20:49:49 +0000 | haftmann | generalized | file | diff | annotate |
| Thu, 09 Nov 2023 15:11:52 +0000 | haftmann | slightly less technical formulation of very specific type class | file | diff | annotate |
| Sat, 16 Sep 2023 06:38:44 +0000 | haftmann | new formulation of an auxiliary lemma | file | diff | annotate |
| Sat, 20 May 2023 14:48:06 +0200 | wenzelm | prefer static simpset; | file | diff | annotate |
| Sat, 20 May 2023 14:12:01 +0200 | wenzelm | omit pointless morphism in global theory; | file | diff | annotate |
| Tue, 24 Jan 2023 10:30:56 +0000 | haftmann | generalized theory name: euclidean division denotes one particular division definition on integers | file | diff | annotate |
| Fri, 28 Oct 2022 06:34:26 +0000 | haftmann | restructured | file | diff | annotate |
| Sun, 21 Aug 2022 06:18:23 +0000 | haftmann | streamlined | file | diff | annotate |
| Tue, 26 Oct 2021 14:43:59 +0000 | haftmann | more generic bit/word lemmas for distribution | file | diff | annotate |
| Mon, 02 Aug 2021 10:01:06 +0000 | haftmann | moved theory Bit_Operations into Main corpus | file | diff | annotate |
| Mon, 12 Jul 2021 11:41:02 +0000 | haftmann | operations for symbolic computation of bit operations | file | diff | annotate |
| Thu, 24 Jun 2021 06:06:32 +0000 | haftmann | more word cleanup | file | diff | annotate |
| Wed, 16 Jun 2021 08:19:09 +0000 | haftmann | more lemmas | file | diff | annotate |
| Tue, 06 Apr 2021 18:12:20 +0000 | haftmann | new lemmas | file | diff | annotate |
| Mon, 30 Nov 2020 17:10:49 +0100 | wenzelm | tuned whitespace --- avoid TABs; | file | diff | annotate |
| Sun, 15 Nov 2020 10:13:03 +0000 | haftmann | official collection for bit projection simplifications | file | diff | annotate |
| Tue, 27 Oct 2020 16:59:44 +0000 | haftmann | more lemmas | file | diff | annotate |
| Wed, 23 Sep 2020 11:14:38 +0000 | haftmann | more thorough treatment of division, particularly signed division on int and word | file | diff | annotate |
| Thu, 17 Sep 2020 09:57:31 +0000 | haftmann | integrated generic conversions into word corpse | file | diff | annotate |
| Thu, 17 Sep 2020 09:57:30 +0000 | haftmann | more lemmas | file | diff | annotate |
| Sat, 05 Sep 2020 08:32:27 +0000 | haftmann | generalized | file | diff | annotate |
| Sun, 30 Aug 2020 15:15:28 +0000 | haftmann | more on conversions | file | diff | annotate |
| Fri, 21 Aug 2020 18:59:30 +0000 | haftmann | more lemmas | file | diff | annotate |
| Sat, 01 Aug 2020 17:43:30 +0000 | haftmann | more consequent transferability | file | diff | annotate |
| Sun, 12 Jul 2020 18:10:06 +0000 | haftmann | more simp rules for concrete numerical values | file | diff | annotate |
| Sat, 11 Jul 2020 18:09:09 +0000 | haftmann | a generic horner sum operation | file | diff | annotate |
| Sat, 11 Jul 2020 18:09:08 +0000 | haftmann | more thms | file | diff | annotate |
| Fri, 03 Jul 2020 06:18:29 +0000 | haftmann | misc lemma tuning | file | diff | annotate |
| Sat, 20 Jun 2020 05:56:28 +0000 | haftmann | simp rules for conversions | file | diff | annotate |
| Sat, 20 Jun 2020 05:56:28 +0000 | haftmann | more class operations for the sake of efficient generated code | file | diff | annotate |
| Thu, 18 Jun 2020 09:07:54 +0000 | haftmann | more lemmas | file | diff | annotate |
| Thu, 21 May 2020 20:00:08 +0000 | haftmann | tuned module name space for generated code | file | diff | annotate |
| Wed, 13 May 2020 12:55:33 +0200 | Manuel Eberl | new constant power_int in HOL | file | diff | annotate |
| Fri, 08 May 2020 06:26:28 +0000 | haftmann | prefer _ mod 2 over of_bool (odd _) | file | diff | annotate |
| Mon, 27 Apr 2020 16:18:51 +0000 | haftmann | simplified construction of binary bit operations | file | diff | annotate |
| Sat, 25 Apr 2020 13:26:24 +0000 | haftmann | more rules | file | diff | annotate |
| Fri, 24 Apr 2020 13:16:41 +0000 | haftmann | numeral rules for take_bit / drop_bit on int | file | diff | annotate |
| Thu, 16 Apr 2020 08:09:31 +0200 | haftmann | more theorems | file | diff | annotate |
| Thu, 16 Apr 2020 08:09:29 +0200 | haftmann | bit on numerals | file | diff | annotate |
| Thu, 16 Apr 2020 08:09:28 +0200 | haftmann | more complete rules on numerals | file | diff | annotate |
| Sun, 08 Mar 2020 17:07:49 +0000 | haftmann | more frugal simp rules for bit operations; more pervasive use of bit selector | file | diff | annotate |
| Tue, 11 Feb 2020 19:03:56 +0100 | haftmann | tuned proof | file | diff | annotate |
| Sun, 09 Feb 2020 22:03:07 +0000 | haftmann | easy abstraction over pointwise bit operations | file | diff | annotate |
| Sun, 09 Feb 2020 10:46:32 +0000 | haftmann | rule concerning bit (push_bit ...) | file | diff | annotate |
| Sun, 09 Feb 2020 10:21:01 +0000 | haftmann | more lemmas | file | diff | annotate |
| Mon, 03 Feb 2020 20:42:04 +0000 | haftmann | more theorems | file | diff | annotate |
| Sat, 01 Feb 2020 19:10:40 +0100 | haftmann | more specific class assumptions | file | diff | annotate |
| Sat, 01 Feb 2020 19:10:37 +0100 | haftmann | more theorems | file | diff | annotate |
| Sun, 26 Jan 2020 20:35:32 +0000 | haftmann | more theorems | file | diff | annotate |
| Mon, 02 Dec 2019 17:15:16 +0000 | haftmann | tuned material | file | diff | annotate |
| Sun, 01 Dec 2019 08:00:59 +0000 | haftmann | characterization of singleton bit operation | file | diff | annotate |
| Wed, 27 Nov 2019 16:54:33 +0000 | haftmann | bit accessor and fundamental properties | file | diff | annotate |
| Sat, 23 Nov 2019 09:56:11 +0000 | haftmann | tuned theory structure | file | diff | annotate |
| Sun, 17 Nov 2019 20:44:35 +0000 | haftmann | strengthened type class for bit operations | file | diff | annotate |
| Sat, 09 Nov 2019 15:39:21 +0000 | haftmann | bit shifts as class operations | file | diff | annotate |
| Thu, 31 Oct 2019 09:02:02 +0000 | haftmann | more lemmas | file | diff | annotate |