Page MenuHomeIsabelle/Phabricator

florian.haftmann (Florian Haftmann)
User

Projects

User Details

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

Recent Activity

Thu, Feb 22

florian.haftmann committed rISABELLEc172eecba85d: simplified specification of type class semiring_bits.
simplified specification of type class semiring_bits
Thu, Feb 22, 8:47 AM

Thu, Feb 15

florian.haftmann committed rISABELLEad29777e8746: more on disjunctive addition/subtraction.
more on disjunctive addition/subtraction
Thu, Feb 15, 8:19 AM
florian.haftmann committed rAFPe76796bc90d8: formally normalized definition of singleton shifts to their primitive form.
formally normalized definition of singleton shifts to their primitive form
Thu, Feb 15, 8:19 AM

Mon, Feb 12

florian.haftmann committed rISABELLEb14c4cb37d99: more lemmas.
more lemmas
Mon, Feb 12, 4:29 PM

Fri, Feb 9

florian.haftmann committed rISABELLE9f22b71e209e: simplified class specification.
simplified class specification
Fri, Feb 9, 9:58 PM
florian.haftmann committed rAFP1fb8eb4d03bc: simplified class specification.
simplified class specification
Fri, Feb 9, 9:56 PM

Wed, Feb 7

florian.haftmann committed rISABELLEdafb3d343cd6: more lemmas and more correct lemma names.
more lemmas and more correct lemma names
Wed, Feb 7, 7:26 PM

Fri, Feb 2

florian.haftmann committed rISABELLE82fbd5919f24: explicit reference to code_dt.
explicit reference to code_dt
Fri, Feb 2, 6:32 AM

Wed, Jan 31

florian.haftmann committed rAFPc86fe3a1d9eb: strengthened class parity.
strengthened class parity
Wed, Jan 31, 1:12 PM
florian.haftmann committed rISABELLE8ef205d9fd22: strengthened class parity.
strengthened class parity
Wed, Jan 31, 1:10 PM

Mon, Jan 29

florian.haftmann committed rAFP6aad2fc5639f: common type class for trivial properties on div/mod.
common type class for trivial properties on div/mod
Mon, Jan 29, 8:56 PM
florian.haftmann committed rISABELLE4f40225936d1: common type class for trivial properties on div/mod.
common type class for trivial properties on div/mod
Mon, Jan 29, 8:55 PM

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
Fri, Jan 26, 8:15 AM
florian.haftmann committed rAFP7d8816406f74: rearranged and reformulated abstract classes for bit structures and operations.
rearranged and reformulated abstract classes for bit structures and operations
Fri, Jan 26, 8:14 AM

Jan 20 2024

florian.haftmann committed rAFPe53559cafaa6: streamlined type class specification.
streamlined type class specification
Jan 20 2024, 9:34 PM
florian.haftmann committed rAFP92eb53e213a7: consolidated lemma name.
consolidated lemma name
Jan 20 2024, 9:34 PM
florian.haftmann committed rAFP56a49eb309da: simplified specification of type class.
simplified specification of type class
Jan 20 2024, 9:34 PM
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 20 2024, 9:34 PM

Jan 15 2024

florian.haftmann committed rISABELLE1e19abf373ac: streamlined type class specification.
streamlined type class specification
Jan 15 2024, 6:14 PM
florian.haftmann committed rISABELLE62d8c6c08fb2: consolidated lemma name.
consolidated lemma name
Jan 15 2024, 6:14 PM

Jan 14 2024

florian.haftmann committed rISABELLE8205977e9e2c: simplified specification of type class.
simplified specification of type class
Jan 14 2024, 10:49 AM
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
Jan 14 2024, 10:49 AM

Dec 3 2023

florian.haftmann committed rISABELLE486a32079c60: compactified specification of type class parity.
compactified specification of type class parity
Dec 3 2023, 5:49 PM
florian.haftmann committed rISABELLE7476818dfd5d: generalized.
generalized
Dec 3 2023, 5:49 PM
florian.haftmann committed rISABELLEb90bf6636260: explicit annotation of lemma duplicates.
explicit annotation of lemma duplicates
Dec 3 2023, 5:49 PM

Nov 28 2023

florian.haftmann committed rISABELLEa91050cd5c93: de-duplicated specification of class ring_bit_operations.
de-duplicated specification of class ring_bit_operations
Nov 28 2023, 9:16 PM
florian.haftmann committed rAFP41e34fa525fe: de-duplicated specification of class ring_bit_operations.
de-duplicated specification of class ring_bit_operations
Nov 28 2023, 9:16 PM

Nov 27 2023

florian.haftmann committed rISABELLE7ab8b3f1d84b: generalized.
generalized
Nov 27 2023, 8:56 AM
florian.haftmann committed rISABELLEa4775fe69f5d: restructured.
restructured
Nov 27 2023, 8:56 AM
florian.haftmann committed rISABELLE48ca09068adf: grouped lemmas for symbolic computations.
grouped lemmas for symbolic computations
Nov 27 2023, 8:56 AM
florian.haftmann committed rISABELLEcb72e2c0c539: sorted out lemma duplicates.
sorted out lemma duplicates
Nov 27 2023, 8:56 AM

Nov 24 2023

florian.haftmann committed rAFPf7e0a078fa7b: slightly more elementary characterization of unset_bit.
slightly more elementary characterization of unset_bit
Nov 24 2023, 8:05 AM
florian.haftmann committed rISABELLE4596a14d9a95: slightly more elementary characterization of unset_bit.
slightly more elementary characterization of unset_bit
Nov 24 2023, 8:03 AM
florian.haftmann committed rISABELLEbdea2b95817b: more direct characterization of binary bit operations.
more direct characterization of binary bit operations
Nov 24 2023, 8:03 AM

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…
Nov 23 2023, 8:02 AM
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 23 2023, 8:02 AM

Nov 22 2023

florian.haftmann committed rISABELLE127ba61b2630: modernized, reordered, generalized.
modernized, reordered, generalized
Nov 22 2023, 8:15 AM
florian.haftmann committed rISABELLE74440d820ba5: more correct type annotation.
more correct type annotation
Nov 22 2023, 8:15 AM
florian.haftmann committed rAFPb7179a3d107c: tuned proof.
tuned proof
Nov 22 2023, 8:14 AM

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
Nov 20 2023, 9:28 AM
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 20 2023, 9:09 AM

Nov 12 2023

florian.haftmann committed rISABELLE74147aa81dbb: more specific name for type class.
more specific name for type class
Nov 12 2023, 3:40 PM

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
Nov 10 2023, 8:43 AM
florian.haftmann committed rISABELLE5e6b195eee83: slightly less technical formulation of very specific type class.
slightly less technical formulation of very specific type class
Nov 10 2023, 8:41 AM
florian.haftmann committed rISABELLE5e788ff7a489: explicit type class for discrete linordered semidoms.
explicit type class for discrete linordered semidoms
Nov 10 2023, 8:41 AM
florian.haftmann committed rISABELLEddf255a4ccc3: weakened dependency.
weakened dependency
Nov 10 2023, 8:41 AM

Sep 16 2023

florian.haftmann committed rAFPfc96173189a3: reduced prominence of lemma names.
reduced prominence of lemma names
Sep 16 2023, 3:38 PM
florian.haftmann committed rISABELLE18ea58bdcf77: reduced prominence of lemma names.
reduced prominence of lemma names
Sep 16 2023, 3:36 PM
florian.haftmann committed rISABELLEd52934f126d4: new formulation of an auxiliary lemma.
new formulation of an auxiliary lemma
Sep 16 2023, 3:36 PM

Sep 14 2023

florian.haftmann committed rISABELLE2ca78c955c97: Corrected type calculation..
Corrected type calculation.
Sep 14 2023, 1:35 PM
florian.haftmann committed rISABELLEb0ddfa5b9ddc: some hints on managed installations.
some hints on managed installations
Sep 14 2023, 7:24 AM
florian.haftmann committed rISABELLEd052d61da398: prefer cartouches over quotes for clarity of resulting document.
prefer cartouches over quotes for clarity of resulting document
Sep 14 2023, 7:24 AM

May 3 2023

florian.haftmann committed rISABELLEf041d5060892: tuned.
tuned
May 3 2023, 8:11 AM
florian.haftmann committed rISABELLEfaaff590bd9e: stripped unused functionality.
stripped unused functionality
May 3 2023, 8:11 AM

May 2 2023

florian.haftmann committed rISABELLEb41c8fce442d: case translation in intermediate language eliminates semantic clone.
case translation in intermediate language eliminates semantic clone
May 2 2023, 7:59 AM

Apr 30 2023

florian.haftmann committed rISABELLE55fb4572e062: more correct type calculation.
more correct type calculation
Apr 30 2023, 8:16 AM
florian.haftmann committed rISABELLE909efe20ff3b: Backed out changeset 5016262a2384.
Backed out changeset 5016262a2384
Apr 30 2023, 8:16 AM
florian.haftmann added a reverting change for rISABELLE5016262a2384: thingol: fix abstraction return types in case: rISABELLE909efe20ff3b: Backed out changeset 5016262a2384.
Apr 30 2023, 8:16 AM

Apr 20 2023

florian.haftmann committed rISABELLE89676df5846a: tuned.
tuned
Apr 20 2023, 8:14 AM
florian.haftmann committed rISABELLE0e054e6e7f5e: clarified terminology.
clarified terminology
Apr 20 2023, 8:14 AM

Apr 11 2023

florian.haftmann committed rAFP0db1121d505f: some remarks on division.
some remarks on division
Apr 11 2023, 11:07 PM
florian.haftmann committed rAFP235048f7f017: no subsection without section.
no subsection without section
Apr 11 2023, 11:07 PM
florian.haftmann committed rAFP17d46502c26f: clarified scope of document.
clarified scope of document
Apr 11 2023, 11:07 PM
florian.haftmann committed rISABELLEfb3d81bd9803: some remarks on division.
some remarks on division
Apr 11 2023, 11:07 PM
florian.haftmann committed rISABELLEae9e6218443d: proper section headings.
proper section headings
Apr 11 2023, 11:07 PM

Mar 24 2023

florian.haftmann committed rAFP8b1d59d0990d: Adjusted to changes in distribution..
Adjusted to changes in distribution.
Mar 24 2023, 8:26 PM
florian.haftmann committed rISABELLEa6a81f848135: More explicit type information in dictionary arguments..
More explicit type information in dictionary arguments.
Mar 24 2023, 8:04 PM
florian.haftmann committed rISABELLE596452389ad0: tuned.
tuned
Mar 24 2023, 8:04 PM
florian.haftmann committed rISABELLEe6ee7af8184c: tuned whitespace.
tuned whitespace
Mar 24 2023, 8:04 PM
florian.haftmann committed rISABELLE4c5297aa18c8: more uniform approach towards satisfied applications.
more uniform approach towards satisfied applications
Mar 24 2023, 8:04 PM
florian.haftmann committed rISABELLE0262155d2743: more uniform approach towards satisfied applications.
more uniform approach towards satisfied applications
Mar 24 2023, 8:04 PM
florian.haftmann committed rISABELLEb5fbe9837aee: tuned.
tuned
Mar 24 2023, 8:04 PM
florian.haftmann committed rISABELLE5af3954ed6cf: tuned.
tuned
Mar 24 2023, 8:04 PM
florian.haftmann committed rISABELLE86b9a405b0cc: Tuned semicolons..
Tuned semicolons.
Mar 24 2023, 8:04 PM

Feb 12 2023

florian.haftmann committed rISABELLE04571037ed33: tuned.
tuned
Feb 12 2023, 1:47 PM
florian.haftmann committed rISABELLE6cad6ed2700a: somehow more clear terminology.
somehow more clear terminology
Feb 12 2023, 1:47 PM
florian.haftmann committed rAFP1479cb0036ed: somehow more clear terminology.
somehow more clear terminology
Feb 12 2023, 1:45 PM

Feb 9 2023

florian.haftmann committed rISABELLEb6f3eb537d91: actually executable enum_all, enum_ex for word.
actually executable enum_all, enum_ex for word
Feb 9 2023, 3:23 PM

Jan 27 2023

florian.haftmann committed rAFP45600ccea74a: dropped reference to dead clone.
dropped reference to dead clone
Jan 27 2023, 7:18 PM
florian.haftmann committed rAFPbcc172c19476: modernized.
modernized
Jan 27 2023, 7:18 PM
florian.haftmann committed rAFP7be2c9c3f37c: removed dead clone.
removed dead clone
Jan 27 2023, 7:18 PM
florian.haftmann committed rAFP897e5e348bf9: Modernized..
Modernized.
Jan 27 2023, 7:17 PM
florian.haftmann committed rAFPc5fcab8016bf: More instances..
More instances.
Jan 27 2023, 7:17 PM
florian.haftmann committed rAFP970e2a3dcdf1: Tuned whitespace..
Tuned whitespace.
Jan 27 2023, 7:17 PM
florian.haftmann committed rAFPce0774eaa992: More correct references..
More correct references.
Jan 27 2023, 7:17 PM
florian.haftmann committed rAFP72313706f65d: Updated references..
Updated references.
Jan 27 2023, 7:17 PM
florian.haftmann committed rISABELLE4c4d40913900: Restored antiquotation..
Restored antiquotation.
Jan 27 2023, 7:17 PM
florian.haftmann committed rISABELLE5ef443fa4a5d: tuned whitespace.
tuned whitespace
Jan 27 2023, 7:16 PM

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…
Jan 24 2023, 12:00 PM
florian.haftmann committed rAFPdb93f67adfd0: generalized theory name: euclidean division denotes one particular division….
generalized theory name: euclidean division denotes one particular division…
Jan 24 2023, 12:00 PM
florian.haftmann committed rAFP75e99d0e6664: more efficient specification.
more efficient specification
Jan 24 2023, 12:00 PM

Dec 17 2022

florian.haftmann committed rISABELLE89f78f76df1c: prefer SML here.
prefer SML here
Dec 17 2022, 10:19 AM
florian.haftmann committed rISABELLE2afbd514b654: Typo..
Typo.
Dec 17 2022, 10:19 AM

Oct 28 2022

florian.haftmann committed rISABELLE8cb141384682: restructured.
restructured
Oct 28 2022, 3:30 PM
florian.haftmann committed rISABELLE6bc3bb9d0e3e: modulus for polynomials is invariant wrt. units.
modulus for polynomials is invariant wrt. units
Oct 28 2022, 3:30 PM

Oct 6 2022

florian.haftmann committed rISABELLEfbde7d1211fc: euclidean division on gaussian numbers.
euclidean division on gaussian numbers
Oct 6 2022, 6:36 PM
florian.haftmann committed rISABELLE63bcec915790: tuned proof.
tuned proof
Oct 6 2022, 6:36 PM

Oct 4 2022

florian.haftmann committed rAFPad6ac3e1e898: slightly less abusive proof pattern.
slightly less abusive proof pattern
Oct 4 2022, 5:50 PM
florian.haftmann committed rISABELLE4a064fad28b2: note on signed division on words.
note on signed division on words
Oct 4 2022, 5:49 PM
florian.haftmann committed rISABELLEda4e57d30579: tuned definition.
tuned definition
Oct 4 2022, 5:49 PM