| Mon, 07 Sep 2020 08:47:28 +0000 |
haftmann |
more on conversions
|
file |
diff |
annotate
|
| Sat, 05 Sep 2020 16:21:16 +0000 |
haftmann |
generalized signed_take_bit
|
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
|
| Mon, 10 Aug 2020 15:34:55 +0000 |
haftmann |
dedicated symbols for code generation, to pave way for generic conversions from and to word
|
file |
diff |
annotate
|
| Mon, 10 Aug 2020 08:27:17 +0200 |
haftmann |
reduced prominence od theory Bits_Int
|
file |
diff |
annotate
|
| Thu, 06 Aug 2020 15:37:14 +0000 |
haftmann |
tailored towards remaining essence
|
file |
diff |
annotate
|
| Wed, 05 Aug 2020 19:06:39 +0200 |
haftmann |
separation of reversed bit lists from other material
|
file |
diff |
annotate
|
| Wed, 05 Aug 2020 08:47:45 +0000 |
haftmann |
further refinement of code equations for mask operation
|
file |
diff |
annotate
|
| Tue, 04 Aug 2020 09:33:05 +0000 |
haftmann |
uniform mask operation
|
file |
diff |
annotate
|
| Sat, 01 Aug 2020 17:43:30 +0000 |
haftmann |
more consequent transferability
|
file |
diff |
annotate
|
| Thu, 16 Jul 2020 04:52:26 +0000 |
haftmann |
tuned grouping
|
file |
diff |
annotate
|
| Thu, 16 Jul 2020 04:52:25 +0000 |
haftmann |
yet another alias
|
file |
diff |
annotate
|
| Sun, 12 Jul 2020 18:10:06 +0000 |
haftmann |
prefer canonically oriented lists of bits and more direct characterizations in definitions
|
file |
diff |
annotate
|
| Sat, 11 Jul 2020 06:21:04 +0000 |
haftmann |
signed_take_bit
|
file |
diff |
annotate
|
| Sat, 11 Jul 2020 06:21:02 +0000 |
haftmann |
more on single-bit operations
|
file |
diff |
annotate
|
| Mon, 06 Jul 2020 10:47:30 +0000 |
haftmann |
separation of traditional bit operations
|
file |
diff |
annotate
|
| Sat, 04 Jul 2020 20:45:24 +0000 |
haftmann |
factored out auxiliary theory
|
file |
diff |
annotate
|
| Sat, 04 Jul 2020 20:45:21 +0000 |
haftmann |
prefer explicit proof
|
file |
diff |
annotate
|
| Fri, 03 Jul 2020 06:18:29 +0000 |
haftmann |
misc lemma tuning
|
file |
diff |
annotate
|
| Fri, 03 Jul 2020 06:18:27 +0000 |
haftmann |
explicit proofs for bit projections
|
file |
diff |
annotate
|
| Wed, 01 Jul 2020 17:32:11 +0000 |
haftmann |
factored out ancient numeral representation
|
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, 18 Jun 2020 09:07:30 +0000 |
haftmann |
build bit operations on word on library theory on bit operations
|
file |
diff |
annotate
|
| Thu, 18 Jun 2020 09:07:30 +0000 |
haftmann |
tweak for code generation
|
file |
diff |
annotate
|
| 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
|
file |
diff |
annotate
|
| Thu, 18 Jun 2020 09:07:30 +0000 |
haftmann |
more lemmas and less name space pollution
|
file |
diff |
annotate
|
| Thu, 18 Jun 2020 09:07:30 +0000 |
haftmann |
canonical bit shifts for word type, leaving duplicates as they are at the moment
|
file |
diff |
annotate
|
| Thu, 18 Jun 2020 09:07:30 +0000 |
haftmann |
essential instance about bit structure
|
file |
diff |
annotate
|
| Thu, 18 Jun 2020 09:07:29 +0000 |
haftmann |
more transfer rules
|
file |
diff |
annotate
|
| Thu, 18 Jun 2020 09:07:29 +0000 |
haftmann |
dropped yet another duplicate
|
file |
diff |
annotate
|
| Thu, 18 Jun 2020 09:07:29 +0000 |
haftmann |
fundamental construction of word type following existing transfer rules
|
file |
diff |
annotate
|
| Thu, 18 Jun 2020 09:07:29 +0000 |
haftmann |
replaced mere alias by input abbreviation
|
file |
diff |
annotate
|
| Thu, 18 Jun 2020 09:07:29 +0000 |
haftmann |
replaced mere alias by abbreviation
|
file |
diff |
annotate
|
| Thu, 18 Jun 2020 09:07:29 +0000 |
haftmann |
replaced operation with weak abstraction by input abbreviation
|
file |
diff |
annotate
|
| Thu, 18 Jun 2020 09:07:29 +0000 |
haftmann |
avoid compound operation
|
file |
diff |
annotate
|
| Thu, 18 Jun 2020 09:07:29 +0000 |
haftmann |
eliminated warnings
|
file |
diff |
annotate
|
| Sat, 09 May 2020 17:20:04 +0000 |
haftmann |
modernized notation for bit operations
|
file |
diff |
annotate
|
| Fri, 22 Nov 2019 09:25:01 +0000 |
haftmann |
proper prefix syntax
|
file |
diff |
annotate
|
| Fri, 18 Oct 2019 18:41:33 +0000 |
haftmann |
moved quickcheck setup to distribution
|
file |
diff |
annotate
|
| Fri, 18 Oct 2019 18:41:31 +0000 |
haftmann |
moved generic instance to distribution
|
file |
diff |
annotate
|
| Tue, 24 Sep 2019 12:56:10 +0100 |
paulson |
More type class generalisations. Note that linorder_antisym_conv1 and linorder_antisym_conv2 no longer exist.
|
file |
diff |
annotate
|
| Fri, 14 Jun 2019 08:34:27 +0000 |
haftmann |
clear separation of types for bits (False / True) and Z2 (0 / 1)
|
file |
diff |
annotate
|
| Mon, 22 Apr 2019 09:33:55 +0000 |
haftmann |
consolidated map2 clones
|
file |
diff |
annotate
|
| Mon, 22 Apr 2019 09:33:55 +0000 |
haftmann |
separate type class for bit comprehension
|
file |
diff |
annotate
|
| Mon, 22 Apr 2019 09:33:55 +0000 |
haftmann |
no need to maintain two separate type classes
|
file |
diff |
annotate
|
| Mon, 22 Apr 2019 06:28:17 +0000 |
haftmann |
clarified structure of theories
|
file |
diff |
annotate
|
| Sat, 20 Apr 2019 18:02:21 +0000 |
haftmann |
avoid separate type class for mere definitional extension
|
file |
diff |
annotate
|
| Sat, 20 Apr 2019 18:02:20 +0000 |
haftmann |
tuned name
|
file |
diff |
annotate
|
| Sat, 20 Apr 2019 13:44:16 +0000 |
haftmann |
clarified notation
|
file |
diff |
annotate
|
| Thu, 18 Apr 2019 06:06:54 +0000 |
haftmann |
incorporated various material from the AFP into the distribution
|
file |
diff |
annotate
|
| Tue, 16 Apr 2019 19:50:20 +0000 |
haftmann |
eliminated type class
|
file |
diff |
annotate
|
| Tue, 16 Apr 2019 19:50:18 +0000 |
haftmann |
tuned theory names
|
file |
diff |
annotate
|
| Tue, 16 Apr 2019 19:50:05 +0000 |
haftmann |
prefer one theory for misc material
|
file |
diff |
annotate
|
| Tue, 16 Apr 2019 19:50:03 +0000 |
haftmann |
moved instance to appropriate place
|
file |
diff |
annotate
|
| Sun, 06 Jan 2019 15:04:34 +0100 |
wenzelm |
isabelle update -u path_cartouches;
|
file |
diff |
annotate
|
| Mon, 24 Sep 2018 14:30:09 +0200 |
nipkow |
Prefix form of infix with * on either side no longer needs special treatment
|
file |
diff |
annotate
|
| Sat, 12 May 2018 22:20:46 +0200 |
haftmann |
removed some non-essential rules
|
file |
diff |
annotate
|
| Tue, 16 Jan 2018 09:30:00 +0100 |
wenzelm |
standardized towards new-style formal comments: isabelle update_comments;
|
file |
diff |
annotate
|