src/HOL/ex/Word.thy
Tue, 04 Aug 2020 09:33:05 +0000 haftmann uniform mask operation
Sat, 01 Aug 2020 17:43:30 +0000 haftmann more consequent transferability
Sat, 11 Jul 2020 06:21:04 +0000 haftmann signed_take_bit
Fri, 03 Jul 2020 06:18:29 +0000 haftmann misc lemma tuning
Sat, 20 Jun 2020 05:56:28 +0000 haftmann more class operations for the sake of efficient generated code
Thu, 18 Jun 2020 09:07:30 +0000 haftmann bit operations as distinctive library theory
Thu, 18 Jun 2020 09:07:30 +0000 haftmann pragmatically ruled out word types of length zero: a bit string with no bits is not bit string at all
Thu, 04 Jun 2020 19:38:50 +0000 haftmann avoid overaggressive default simp rules
Thu, 21 May 2020 20:00:09 +0000 haftmann slightly more specific implementations
Fri, 08 May 2020 06:26:28 +0000 haftmann prefer _ mod 2 over of_bool (odd _)
Thu, 16 Apr 2020 08:09:32 +0200 haftmann generalized
Sun, 08 Mar 2020 17:07:49 +0000 haftmann more frugal simp rules for bit operations; more pervasive use of bit selector
Thu, 13 Feb 2020 07:43:48 +0100 haftmann canonical approach towards lifting
Sun, 09 Feb 2020 10:46:32 +0000 haftmann rule concerning bit (push_bit ...)
Mon, 03 Feb 2020 20:42:04 +0000 haftmann more theorems
Sat, 01 Feb 2020 19:10:40 +0100 haftmann more specific class assumptions
Sat, 01 Feb 2020 19:10:37 +0100 haftmann more theorems
Sun, 26 Jan 2020 20:35:32 +0000 haftmann sketches of ideas still to come
Mon, 02 Dec 2019 17:15:17 +0000 haftmann more rules
Mon, 02 Dec 2019 17:15:16 +0000 haftmann tuned material
Sun, 01 Dec 2019 17:51:23 +0000 haftmann characterization of typical bit operations
Sun, 01 Dec 2019 08:01:00 +0000 haftmann transfer rule for bit operation
Sun, 01 Dec 2019 08:00:59 +0000 haftmann characterization of singleton bit operation
Wed, 27 Nov 2019 16:54:33 +0000 haftmann bit accessor and fundamental properties
Sun, 17 Nov 2019 20:44:35 +0000 haftmann strengthened type class for bit operations
Mon, 11 Nov 2019 07:16:17 +0000 haftmann tuned order between theories
Sat, 09 Nov 2019 15:39:21 +0000 haftmann bit shifts as class operations
Sat, 09 Nov 2019 10:38:51 +0000 haftmann new lemma
Mon, 04 Nov 2019 20:38:15 +0000 haftmann proof-of-concept theory for bit operations without a constructivistic representation and a minimal common logical foundation
less more (0) tip