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
|
Fri, 12 Jan 2018 15:27:46 +0100 |
wenzelm |
prefer formal comments;
|
file |
diff |
annotate
|
Wed, 10 Jan 2018 15:25:09 +0100 |
nipkow |
ran isabelle update_op on all sources
|
file |
diff |
annotate
|
Sun, 03 Dec 2017 19:09:42 +0100 |
wenzelm |
simplified session (again, see 39e29972cb96): WordExamples requires < 1s;
|
file |
diff |
annotate
|
Sat, 02 Dec 2017 16:50:53 +0000 |
haftmann |
more simplification rules
|
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
|
Sun, 08 Oct 2017 22:28:21 +0200 |
haftmann |
elementary definition of division on natural numbers
|
file |
diff |
annotate
|
Fri, 18 Aug 2017 20:47:47 +0200 |
wenzelm |
session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
|
file |
diff |
annotate
|
Mon, 03 Apr 2017 23:12:16 +0200 |
wenzelm |
misc tuning and modernization;
|
file |
diff |
annotate
|