# User Details

User Details

- User Since
- Nov 30 2019, 9:26 AM (221 w, 26 m)

# Thu, Feb 22

Thu, Feb 22

florian.haftmann committed rISABELLEc172eecba85d: simplified specification of type class semiring_bits.

simplified specification of type class semiring_bits

# Thu, Feb 15

Thu, Feb 15

more on disjunctive addition/subtraction

florian.haftmann committed rAFPe76796bc90d8: formally normalized definition of singleton shifts to their primitive form.

formally normalized definition of singleton shifts to their primitive form

# Mon, Feb 12

Mon, Feb 12

# Fri, Feb 9

Fri, Feb 9

simplified class specification

simplified class specification

# Wed, Feb 7

Wed, Feb 7

more lemmas and more correct lemma names

# Fri, Feb 2

Fri, Feb 2

explicit reference to code_dt

# Wed, Jan 31

Wed, Jan 31

strengthened class parity

strengthened class parity

# Mon, Jan 29

Mon, Jan 29

common type class for trivial properties on div/mod

florian.haftmann committed rISABELLE4f40225936d1: common type class for trivial properties on div/mod.

common type class for trivial properties on div/mod

# Fri, Jan 26

Fri, Jan 26

florian.haftmann committed rISABELLE22a137a6de44: rearranged and reformulated abstract classes for bit structures and operations.

rearranged and reformulated abstract classes for bit structures and operations

florian.haftmann committed rAFP7d8816406f74: rearranged and reformulated abstract classes for bit structures and operations.

rearranged and reformulated abstract classes for bit structures and operations

# Jan 20 2024

Jan 20 2024

streamlined type class specification

consolidated lemma name

simplified specification of type class

florian.haftmann committed rAFP3dd60aa86a62: consolidated name of lemma analogously to nat/int/word_bit_induct.

consolidated name of lemma analogously to nat/int/word_bit_induct

# Jan 15 2024

Jan 15 2024

streamlined type class specification

consolidated lemma name

# Jan 14 2024

Jan 14 2024

simplified specification of type class

florian.haftmann committed rISABELLEc7cb1bf6efa0: consolidated name of lemma analogously to nat/int/word_bit_induct.

consolidated name of lemma analogously to nat/int/word_bit_induct

# Dec 3 2023

Dec 3 2023

compactified specification of type class parity

explicit annotation of lemma duplicates

# Nov 28 2023

Nov 28 2023

florian.haftmann committed rISABELLEa91050cd5c93: de-duplicated specification of class ring_bit_operations.

de-duplicated specification of class ring_bit_operations

florian.haftmann committed rAFP41e34fa525fe: de-duplicated specification of class ring_bit_operations.

de-duplicated specification of class ring_bit_operations

# Nov 27 2023

Nov 27 2023

grouped lemmas for symbolic computations

sorted out lemma duplicates

# Nov 24 2023

Nov 24 2023

florian.haftmann committed rAFPf7e0a078fa7b: slightly more elementary characterization of unset_bit.

slightly more elementary characterization of unset_bit

florian.haftmann committed rISABELLE4596a14d9a95: slightly more elementary characterization of unset_bit.

slightly more elementary characterization of unset_bit

florian.haftmann committed rISABELLEbdea2b95817b: more direct characterization of binary bit operations.

more direct characterization of binary bit operations

# Nov 23 2023

Nov 23 2023

florian.haftmann committed rISABELLE7449ff77029e: base abstract specification of NOT on recursive equation rather than bit….

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

florian.haftmann committed rAFP608f10ad4828: base abstract specification of NOT on recursive equation rather than bit….

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

# Nov 22 2023

Nov 22 2023

modernized, reordered, generalized

more correct type annotation

# Nov 20 2023

Nov 20 2023

florian.haftmann committed rAFP28289b02b23b: operations AND, OR, XOR are specified by characteristic recursive equation.

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

florian.haftmann committed rISABELLE74a4776f7a22: operations AND, OR, XOR are specified by characteristic recursive equation.

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

# Nov 12 2023

Nov 12 2023

more specific name for type class

# Nov 10 2023

Nov 10 2023

florian.haftmann committed rAFP7cc49d3407b3: slightly less technical formulation of very specific type class.

slightly less technical formulation of very specific type class

florian.haftmann committed rISABELLE5e6b195eee83: slightly less technical formulation of very specific type class.

slightly less technical formulation of very specific type class

florian.haftmann committed rISABELLE5e788ff7a489: explicit type class for discrete linordered semidoms.

explicit type class for discrete linordered semidoms

weakened dependency

# Sep 16 2023

Sep 16 2023

reduced prominence of lemma names

reduced prominence of lemma names

new formulation of an auxiliary lemma

# Sep 14 2023

Sep 14 2023

Corrected type calculation.

some hints on managed installations

florian.haftmann committed rISABELLEd052d61da398: prefer cartouches over quotes for clarity of resulting document.

prefer cartouches over quotes for clarity of resulting document

# May 3 2023

May 3 2023

stripped unused functionality

# May 2 2023

May 2 2023

florian.haftmann committed rISABELLEb41c8fce442d: case translation in intermediate language eliminates semantic clone.

case translation in intermediate language eliminates semantic clone

# Apr 30 2023

Apr 30 2023

more correct type calculation

Backed out changeset 5016262a2384

# Apr 20 2023

Apr 20 2023

clarified terminology

# Apr 11 2023

Apr 11 2023

some remarks on division

no subsection without section

clarified scope of document

some remarks on division

proper section headings

# Mar 24 2023

Mar 24 2023

Adjusted to changes in distribution.

florian.haftmann committed rISABELLEa6a81f848135: More explicit type information in dictionary arguments..

More explicit type information in dictionary arguments.

tuned whitespace

florian.haftmann committed rISABELLE4c5297aa18c8: more uniform approach towards satisfied applications.

more uniform approach towards satisfied applications

florian.haftmann committed rISABELLE0262155d2743: more uniform approach towards satisfied applications.

more uniform approach towards satisfied applications

Tuned semicolons.

# Feb 12 2023

Feb 12 2023

somehow more clear terminology

somehow more clear terminology

# Feb 9 2023

Feb 9 2023

actually executable enum_all, enum_ex for word

# Jan 27 2023

Jan 27 2023

dropped reference to dead clone

removed dead clone

Tuned whitespace.

More correct references.

Updated references.

Restored antiquotation.

tuned whitespace

# Jan 24 2023

Jan 24 2023

florian.haftmann committed rISABELLE5de3772609ea: generalized theory name: euclidean division denotes one particular division….

generalized theory name: euclidean division denotes one particular division…

florian.haftmann committed rAFPdb93f67adfd0: generalized theory name: euclidean division denotes one particular division….

generalized theory name: euclidean division denotes one particular division…

more efficient specification

# Dec 17 2022

Dec 17 2022

prefer SML here

# Oct 28 2022

Oct 28 2022

modulus for polynomials is invariant wrt. units

# Oct 6 2022

Oct 6 2022

euclidean division on gaussian numbers

# Oct 4 2022

Oct 4 2022

slightly less abusive proof pattern

note on signed division on words

tuned definition