Page MenuHomeIsabelle/Phabricator

florian.haftmann (Florian Haftmann)
User

Projects

User Details

User Since
Nov 30 2019, 9:26 AM (43 w, 4 d)

Recent Activity

Fri, Sep 25

florian.haftmann committed rISABELLE4a58c38b85ff: factored out typedef material.
factored out typedef material
Fri, Sep 25, 7:48 AM
florian.haftmann committed rAFP02fd702f6290: factored out typedef material.
factored out typedef material
Fri, Sep 25, 7:47 AM

Wed, Sep 23

florian.haftmann committed rAFPf04759177a5d: canonical enum instance for word.
canonical enum instance for word
Wed, Sep 23, 1:19 PM
florian.haftmann committed rAFPc5f056d78406: more thorough treatment of division, particularly signed division on int and….
more thorough treatment of division, particularly signed division on int and…
Wed, Sep 23, 1:19 PM
florian.haftmann committed rISABELLEbeeadb35e357: more thorough treatment of division, particularly signed division on int and….
more thorough treatment of division, particularly signed division on int and…
Wed, Sep 23, 1:18 PM
florian.haftmann committed rISABELLEdb43ee05066d: canonical enum instance for word.
canonical enum instance for word
Wed, Sep 23, 1:18 PM

Sun, Sep 20

florian.haftmann committed rAFPb3e61e86eff9: identified operation alias; tuned.
identified operation alias; tuned
Sun, Sep 20, 8:49 AM

Thu, Sep 17

florian.haftmann committed rAFPefbce6681b7a: dropped junk.
dropped junk
Thu, Sep 17, 2:28 PM
florian.haftmann committed rISABELLEff32ddc8165c: dropped junk.
dropped junk
Thu, Sep 17, 2:28 PM
florian.haftmann committed rISABELLE47253b1a31ed: typo.
typo
Thu, Sep 17, 1:55 PM
florian.haftmann committed rISABELLEc0a552515c29: NEWS and CONTRIBUTORS.
NEWS and CONTRIBUTORS
Thu, Sep 17, 12:06 PM
florian.haftmann committed rISABELLEa282abb07642: integrated generic conversions into word corpse.
integrated generic conversions into word corpse
Thu, Sep 17, 12:04 PM
florian.haftmann committed rISABELLE5193570b739a: more lemmas.
more lemmas
Thu, Sep 17, 12:04 PM
florian.haftmann committed rAFP58bc7e81bc7f: integrated generic conversions into word corpse.
integrated generic conversions into word corpse
Thu, Sep 17, 12:02 PM
florian.haftmann committed rAFP85d5b6c0bb92: adjusted to changes in distribution.
adjusted to changes in distribution
Thu, Sep 17, 12:02 PM
florian.haftmann committed rAFPf682365c61ce: tuned proof.
tuned proof
Thu, Sep 17, 11:37 AM

Tue, Sep 8

florian.haftmann committed rISABELLE4b011fa5e83b: restructured.
restructured
Tue, Sep 8, 1:52 PM
florian.haftmann committed rISABELLEeaac77208cf9: tuned theory structure.
tuned theory structure
Tue, Sep 8, 8:02 AM

Mon, Sep 7

florian.haftmann committed rISABELLEbb002df3e82e: more on conversions.
more on conversions
Mon, Sep 7, 11:52 AM

Sat, Sep 5

florian.haftmann committed rISABELLE5a6d8675bf4b: generalized signed_take_bit.
generalized signed_take_bit
Sat, Sep 5, 7:28 PM
florian.haftmann committed rISABELLEbb88e31220af: more on conversions.
more on conversions
Sat, Sep 5, 7:28 PM
florian.haftmann committed rISABELLE12e94c2ff6c5: generalized.
generalized
Sat, Sep 5, 7:28 PM
florian.haftmann committed rAFP21bc345f5a27: generalized signed_take_bit.
generalized signed_take_bit
Sat, Sep 5, 7:27 PM
florian.haftmann committed rAFP3c01c6d69e78: more on conversions.
more on conversions
Sat, Sep 5, 7:27 PM

Aug 30 2020

florian.haftmann committed rAFP023af1e22f70: more on conversions.
more on conversions
Aug 30 2020, 8:32 PM
florian.haftmann committed rISABELLE0f3d24dc197f: more on conversions.
more on conversions
Aug 30 2020, 8:30 PM

Aug 24 2020

florian.haftmann committed rAFPa41d53bc4c69: a proof of concept for generic conversions.
a proof of concept for generic conversions
Aug 24 2020, 3:48 PM
florian.haftmann committed rISABELLE7ffa26f05c72: a proof of concept for generic conversions.
a proof of concept for generic conversions
Aug 24 2020, 3:46 PM

Aug 22 2020

florian.haftmann committed rISABELLEe4aecb0c7296: more lemmas.
more lemmas
Aug 22 2020, 8:13 AM
florian.haftmann committed rISABELLEbdf77466b6c8: proper syntax declaration.
proper syntax declaration
Aug 22 2020, 8:13 AM
florian.haftmann committed rAFPa7b99e8a1d84: tuned.
tuned
Aug 22 2020, 8:12 AM

Aug 10 2020

florian.haftmann committed rAFP9a9bc053eb71: dedicated symbols for code generation, to pave way for generic conversions from….
dedicated symbols for code generation, to pave way for generic conversions from…
Aug 10 2020, 6:15 PM
florian.haftmann committed rISABELLE9e5862223442: dedicated symbols for code generation, to pave way for generic conversions from….
dedicated symbols for code generation, to pave way for generic conversions from…
Aug 10 2020, 6:15 PM
florian.haftmann committed rISABELLE9e0321263eb3: consolidated names.
consolidated names
Aug 10 2020, 6:15 PM
florian.haftmann committed rISABELLE3707cf7b370b: reduced prominence od theory Bits_Int.
reduced prominence od theory Bits_Int
Aug 10 2020, 6:15 PM

Aug 6 2020

florian.haftmann committed rAFP116a82414c28: dropped alias.
dropped alias
Aug 6 2020, 11:05 PM
florian.haftmann committed rISABELLE0b21b2beadb5: tailored towards remaining essence.
tailored towards remaining essence
Aug 6 2020, 11:05 PM

Aug 5 2020

florian.haftmann committed rISABELLEa36db1c8238e: separation of reversed bit lists from other material.
separation of reversed bit lists from other material
Aug 5 2020, 7:07 PM
florian.haftmann committed rAFP3e79743d7844: separation of reversed bit lists from other material.
separation of reversed bit lists from other material
Aug 5 2020, 7:07 PM
florian.haftmann committed rAFPcac1c67360f3: further refinement of code equations for mask operation.
further refinement of code equations for mask operation
Aug 5 2020, 1:05 PM
florian.haftmann committed rISABELLE3ec876181527: further refinement of code equations for mask operation.
further refinement of code equations for mask operation
Aug 5 2020, 1:05 PM

Aug 4 2020

florian.haftmann committed rISABELLE41393ecb57ac: uniform mask operation.
uniform mask operation
Aug 4 2020, 3:26 PM
florian.haftmann committed rISABELLEe4d42f5766dc: clearer separation of pre-word bit list material.
clearer separation of pre-word bit list material
Aug 4 2020, 3:25 PM
florian.haftmann committed rAFPf28d68deefa8: uniform mask operation.
uniform mask operation
Aug 4 2020, 3:25 PM
florian.haftmann committed rAFP52ddcd32c0c9: clearer separation of pre-word bit list material.
clearer separation of pre-word bit list material
Aug 4 2020, 3:25 PM
florian.haftmann committed rAFP9b629e0e6654: repaired document slip.
repaired document slip
Aug 4 2020, 7:22 AM

Aug 1 2020

florian.haftmann committed rAFPef3c8932106a: more consequent transferability.
more consequent transferability
Aug 1 2020, 9:18 PM
florian.haftmann committed rISABELLE8c355e2dd7db: more consequent transferability.
more consequent transferability
Aug 1 2020, 8:55 PM

Jul 16 2020

florian.haftmann committed rISABELLEb8bcdb884651: tuned grouping.
tuned grouping
Jul 16 2020, 11:50 AM
florian.haftmann committed rISABELLE587d4681240c: yet another alias.
yet another alias
Jul 16 2020, 11:50 AM

Jul 13 2020

florian.haftmann committed rISABELLE08f1e4cb735f: concatentation of bit values.
concatentation of bit values
Jul 13 2020, 7:25 PM
florian.haftmann committed rAFPce2c72a0a05e: concatentation of bit values.
concatentation of bit values
Jul 13 2020, 7:23 PM
florian.haftmann committed rISABELLE759532ef0885: prefer canonically oriented lists of bits and more direct characterizations in….
prefer canonically oriented lists of bits and more direct characterizations in…
Jul 13 2020, 8:08 AM
florian.haftmann committed rISABELLE5689f0db4508: more simp rules for concrete numerical values.
more simp rules for concrete numerical values
Jul 13 2020, 8:08 AM
florian.haftmann committed rISABELLEb4ed07cbe954: words added to code generator test.
words added to code generator test
Jul 13 2020, 8:08 AM
florian.haftmann committed rAFP7b844df07b1c: prefer canonically oriented lists of bits in definitions.
prefer canonically oriented lists of bits in definitions
Jul 13 2020, 8:07 AM

Jul 11 2020

florian.haftmann committed rISABELLE9b4135e8bade: a generic horner sum operation.
a generic horner sum operation
Jul 11 2020, 11:17 PM
florian.haftmann committed rISABELLE08348e364739: more thms.
more thms
Jul 11 2020, 11:17 PM
florian.haftmann committed rISABELLEfebdd4eead56: more on single-bit operations.
more on single-bit operations
Jul 11 2020, 9:15 AM
florian.haftmann committed rISABELLEa851ce626b78: signed_take_bit.
signed_take_bit
Jul 11 2020, 9:15 AM
florian.haftmann committed rAFP70ae335403b7: signed_take_bit.
signed_take_bit
Jul 11 2020, 9:14 AM

Jul 6 2020

florian.haftmann committed rAFP1cdcce397e9d: separation of traditional bit operations.
separation of traditional bit operations
Jul 6 2020, 1:04 PM
florian.haftmann committed rISABELLE379d0c207c29: separation of traditional bit operations.
separation of traditional bit operations
Jul 6 2020, 1:03 PM

Jul 5 2020

florian.haftmann committed rISABELLE4a013c92a091: factored out auxiliary theory.
factored out auxiliary theory
Jul 5 2020, 8:04 AM
florian.haftmann committed rISABELLEc7ac6d4f3914: prefer explicit proof.
prefer explicit proof
Jul 5 2020, 8:04 AM
florian.haftmann committed rAFPa03e9b5d8dc9: factored out auxiliary theory.
factored out auxiliary theory
Jul 5 2020, 8:04 AM

Jul 3 2020

florian.haftmann committed rISABELLE8bff286878bf: misc lemma tuning.
misc lemma tuning
Jul 3 2020, 12:11 PM
florian.haftmann committed rISABELLE66beb9d92e43: explicit proofs for bit projections.
explicit proofs for bit projections
Jul 3 2020, 12:11 PM
florian.haftmann committed rAFPf90f9d593a88: misc lemma tuning.
misc lemma tuning
Jul 3 2020, 12:10 PM

Jul 2 2020

florian.haftmann committed rAFP81a8bf702c09: activated simproc defined_all.
activated simproc defined_all
Jul 2 2020, 6:13 PM
florian.haftmann committed rISABELLEbad75618fb82: extraction of equations x = t from premises beneath meta-all.
extraction of equations x = t from premises beneath meta-all
Jul 2 2020, 6:12 PM
florian.haftmann committed rAFPe0714a129570: updated documentation.
updated documentation
Jul 2 2020, 4:29 PM
florian.haftmann committed rAFPb8a6808299e5: obsolete duplicates.
obsolete duplicates
Jul 2 2020, 2:10 PM
florian.haftmann committed rISABELLEec17263ec38d: removed superfluous dependency.
removed superfluous dependency
Jul 2 2020, 2:09 PM
florian.haftmann committed rISABELLEace45a11a45e: a small aggiornamento for Z2.
a small aggiornamento for Z2
Jul 2 2020, 2:09 PM
florian.haftmann committed rAFP3ceb3fe8ab08: factored out ancient numeral representation.
factored out ancient numeral representation
Jul 2 2020, 9:14 AM
florian.haftmann committed rAFP82e10d1ca9e1: moved to Word_Lib.
moved to Word_Lib
Jul 2 2020, 9:14 AM
florian.haftmann committed rAFP04f54c116f30: tuned whitespace.
tuned whitespace
Jul 2 2020, 9:14 AM
florian.haftmann committed rISABELLE76193dd4aec8: factored out ancient numeral representation.
factored out ancient numeral representation
Jul 2 2020, 9:14 AM
florian.haftmann committed rISABELLEa1cf296a7786: moved to Word_Lib.
moved to Word_Lib
Jul 2 2020, 9:14 AM
florian.haftmann committed rISABELLE10a8d943a8d8: more explicit proofs.
more explicit proofs
Jul 2 2020, 9:14 AM

Jun 20 2020

florian.haftmann committed rISABELLEe18e9ac8c205: simp rules for conversions.
simp rules for conversions
Jun 20 2020, 9:12 AM
florian.haftmann committed rISABELLEd45f5d4c41bd: more class operations for the sake of efficient generated code.
more class operations for the sake of efficient generated code
Jun 20 2020, 9:12 AM
florian.haftmann committed rAFP0362f33fb949: more class operations for the sake of efficient generated code.
more class operations for the sake of efficient generated code
Jun 20 2020, 9:12 AM

Jun 19 2020

florian.haftmann committed rISABELLEee2c7f0dd1be: prefer single name.
prefer single name
Jun 19 2020, 5:49 PM
florian.haftmann committed rAFPd717807c8843: prefer single name.
prefer single name
Jun 19 2020, 5:48 PM

Jun 18 2020

florian.haftmann committed rAFPd5522275e109: build bit operations on word on library theory on bit operations.
build bit operations on word on library theory on bit operations
Jun 18 2020, 7:16 PM
florian.haftmann committed rAFPc47d97b64977: more instances for uint types.
more instances for uint types
Jun 18 2020, 7:16 PM
florian.haftmann committed rAFP25bc16f7e44a: canonical bit shifts for word type, leaving duplicates as they are at the moment.
canonical bit shifts for word type, leaving duplicates as they are at the moment
Jun 18 2020, 7:16 PM
florian.haftmann committed rAFPae31a7712d9c: dropped yet another duplicate.
dropped yet another duplicate
Jun 18 2020, 7:16 PM
florian.haftmann committed rAFP20b49280a650: replaced mere alias by input abbreviation.
replaced mere alias by input abbreviation
Jun 18 2020, 7:16 PM
florian.haftmann committed rAFPcf6da1bed594: replaced mere alias by abbreviation.
replaced mere alias by abbreviation
Jun 18 2020, 7:16 PM
florian.haftmann committed rAFP23e6a075730d: replaced operation with weak abstraction by input abbreviation.
replaced operation with weak abstraction by input abbreviation
Jun 18 2020, 7:16 PM
florian.haftmann committed rAFP320af0a4f22c: avoid compound operation.
avoid compound operation
Jun 18 2020, 7:16 PM
florian.haftmann committed rAFPbd201908b618: replaced mere alias by input abbreviation.
replaced mere alias by input abbreviation
Jun 18 2020, 7:16 PM
florian.haftmann committed rISABELLE4320875eb8a1: more lemmas.
more lemmas
Jun 18 2020, 7:15 PM
florian.haftmann committed rISABELLEa4bffc0de967: bit operations as distinctive library theory.
bit operations as distinctive library theory
Jun 18 2020, 7:15 PM
florian.haftmann committed rISABELLE3e162c63371a: build bit operations on word on library theory on bit operations.
build bit operations on word on library theory on bit operations
Jun 18 2020, 7:15 PM
florian.haftmann committed rISABELLEa9f913d17d00: tweak for code generation.
tweak for code generation
Jun 18 2020, 7:15 PM
florian.haftmann committed rISABELLE13bb3f5cdc5b: pragmatically ruled out word types of length zero: a bit string with no bits is….
pragmatically ruled out word types of length zero: a bit string with no bits is…
Jun 18 2020, 7:15 PM