src/HOL/Code_Numeral.thy
Mon, 13 Sep 2021 14:18:24 +0000 haftmann explicit predicate for confined bit range avoids cyclic rewriting in presence of extensionality rule for bit values (contributed by Thomas Sewell)
Tue, 03 Aug 2021 13:53:22 +0000 haftmann simplified hierarchy of type classes for bit operations
Mon, 02 Aug 2021 10:01:06 +0000 haftmann moved theory Bit_Operations into Main corpus
Sat, 20 Jun 2020 05:56:28 +0000 haftmann more class operations for the sake of efficient generated code
Sun, 08 Mar 2020 17:07:49 +0000 haftmann more frugal simp rules for bit operations; more pervasive use of bit selector
Sun, 09 Feb 2020 10:46:32 +0000 haftmann rule concerning bit (push_bit ...)
Sat, 01 Feb 2020 19:10:40 +0100 haftmann more specific class assumptions
Mon, 02 Dec 2019 17:15:16 +0000 haftmann tuned material
Sun, 01 Dec 2019 08:00:59 +0000 haftmann characterization of singleton bit operation
Sun, 17 Nov 2019 20:44:35 +0000 haftmann strengthened type class for bit operations
Sat, 09 Nov 2019 15:39:21 +0000 haftmann bit shifts as class operations
Wed, 23 Oct 2019 16:09:23 +0000 haftmann tuned syntax
Fri, 14 Jun 2019 08:34:27 +0000 haftmann slightly more specialized name for type class
Sat, 30 Mar 2019 15:37:22 +0100 haftmann irrelevant
Thu, 28 Mar 2019 21:24:55 +0100 wenzelm "export_code ... file_prefix ..." is the preferred way to produce output within the logical file-system within the theory context, as well as session exports;
less more (0) -100 -15 tip