| Fri, 14 Jun 2019 08:34:28 +0000 |
haftmann |
tuned proofs
|
changeset |
files
|
| Fri, 14 Jun 2019 08:34:27 +0000 |
haftmann |
avoid pseudo-collection to be used in generated proofs
|
changeset |
files
|
| Fri, 14 Jun 2019 08:34:27 +0000 |
haftmann |
moved comment to approproiate place
|
changeset |
files
|
| Fri, 14 Jun 2019 08:34:27 +0000 |
haftmann |
removed outcommented example which seems not to work as advertized
|
changeset |
files
|
| Fri, 14 Jun 2019 08:34:27 +0000 |
haftmann |
clear separation of types for bits (False / True) and Z2 (0 / 1)
|
changeset |
files
|
| Fri, 14 Jun 2019 08:34:27 +0000 |
haftmann |
generalized type classes for parity to cover word types also, which contain zero divisors
|
changeset |
files
|
| Fri, 14 Jun 2019 08:34:27 +0000 |
haftmann |
slightly more specialized name for type class
|
changeset |
files
|
| Fri, 14 Jun 2019 08:34:27 +0000 |
haftmann |
dropped weaker legacy alias
|
changeset |
files
|
| Fri, 14 Jun 2019 08:34:27 +0000 |
haftmann |
slightly more stringent ordering of theorems
|
changeset |
files
|
| Fri, 14 Jun 2019 08:34:27 +0000 |
haftmann |
removed relics of ASCII syntax for indexed big operators
|
changeset |
files
|
| Fri, 14 Jun 2019 08:34:27 +0000 |
haftmann |
dropped former legacy input abbreviations
|
changeset |
files
|
| Fri, 14 Jun 2019 08:34:27 +0000 |
haftmann |
using (*)-syntax for partially applied infix is fine, contrary to ancient op-syntax
|
changeset |
files
|
| Fri, 14 Jun 2019 08:34:27 +0000 |
haftmann |
prefer fixed simpset for proof procedure
|
changeset |
files
|
| Fri, 14 Jun 2019 08:34:27 +0000 |
haftmann |
tuned file system structure
|
changeset |
files
|
| Fri, 14 Jun 2019 08:34:27 +0000 |
haftmann |
avoid spammed sledgehammer proofs
|
changeset |
files
|
| Tue, 11 Jun 2019 18:33:27 +0200 |
nipkow |
added lemmas
|
changeset |
files
|