prefer canonical theorem name for fact collection declarations

avoid [no_atp] declations shadowing propositions from sledgehammer

Tuned proofs

simplified specification of type class semiring_bits

more on disjunctive addition/subtraction

formally normalized definition of singleton shifts to their primitive form

more lemmas

simplified class specification

simplified class specification

more lemmas and more correct lemma names

explicit reference to code_dt

strengthened class parity

strengthened class parity

common type class for trivial properties on div/mod

common type class for trivial properties on div/mod

rearranged and reformulated abstract classes for bit structures and operations

rearranged and reformulated abstract classes for bit structures and operations

streamlined type class specification

consolidated lemma name

simplified specification of type class

consolidated name of lemma analogously to nat/int/word_bit_induct

streamlined type class specification

consolidated lemma name

simplified specification of type class

consolidated name of lemma analogously to nat/int/word_bit_induct

compactified specification of type class parity

generalized

explicit annotation of lemma duplicates

de-duplicated specification of class ring_bit_operations

de-duplicated specification of class ring_bit_operations

generalized

restructured

grouped lemmas for symbolic computations

sorted out lemma duplicates

slightly more elementary characterization of unset_bit

slightly more elementary characterization of unset_bit

more direct characterization of binary bit operations

base abstract specification of NOT on recursive equation rather than bit…

base abstract specification of NOT on recursive equation rather than bit…

modernized, reordered, generalized

more correct type annotation

tuned proof

operations AND, OR, XOR are specified by characteristic recursive equation

operations AND, OR, XOR are specified by characteristic recursive equation

more specific name for type class

slightly less technical formulation of very specific type class

slightly less technical formulation of very specific type class

explicit type class for discrete linordered semidoms

weakened dependency

reduced prominence of lemma names

reduced prominence of lemma names

new formulation of an auxiliary lemma

Corrected type calculation.

some hints on managed installations

prefer cartouches over quotes for clarity of resulting document

tuned

stripped unused functionality

case translation in intermediate language eliminates semantic clone

more correct type calculation

Backed out changeset 5016262a2384

tuned

clarified terminology

some remarks on division

no subsection without section

clarified scope of document

some remarks on division

proper section headings

Adjusted to changes in distribution.

More explicit type information in dictionary arguments.

tuned

tuned whitespace

more uniform approach towards satisfied applications

more uniform approach towards satisfied applications

tuned

tuned

Tuned semicolons.

tuned

somehow more clear terminology

somehow more clear terminology

actually executable enum_all, enum_ex for word

dropped reference to dead clone

modernized

removed dead clone

Modernized.

More instances.

Tuned whitespace.

More correct references.

Updated references.

Restored antiquotation.

tuned whitespace

generalized theory name: euclidean division denotes one particular division…

generalized theory name: euclidean division denotes one particular division…

more efficient specification

prefer SML here

Typo.

restructured

modulus for polynomials is invariant wrt. units

euclidean division on gaussian numbers

tuned proof