Page MenuHomeIsabelle/Phabricator

florian.haftmann (Florian Haftmann)
User

Projects

User Details

User Since
Nov 30 2019, 9:26 AM (46 w, 2 d)

Recent Activity

Sat, Oct 17

florian.haftmann committed rAFP358b66dce878: guide continued.
guide continued
Sat, Oct 17, 7:16 PM
florian.haftmann committed rAFP19a0ae99e1d8: factored out theory Bits_Int.
factored out theory Bits_Int
Sat, Oct 17, 7:16 PM
florian.haftmann committed rISABELLEa1366ce41368: early and more complete setup of tools.
early and more complete setup of tools
Sat, Oct 17, 7:14 PM
florian.haftmann committed rISABELLEee659bca8955: factored out theory Bits_Int.
factored out theory Bits_Int
Sat, Oct 17, 7:14 PM
florian.haftmann committed rISABELLEab32922f139b: factored out singular operation into separate theory.
factored out singular operation into separate theory
Sat, Oct 17, 7:14 PM

Mon, Oct 12

florian.haftmann committed rISABELLEe4dde7beab39: dedicated module for toplevel target handling.
dedicated module for toplevel target handling
Mon, Oct 12, 9:47 AM
florian.haftmann committed rISABELLE24bd1316eaae: consolidated names and operations.
consolidated names and operations
Mon, Oct 12, 9:47 AM
florian.haftmann committed rISABELLEe51f1733618d: replaced combinators by more conventional nesting pattern.
replaced combinators by more conventional nesting pattern
Mon, Oct 12, 9:47 AM
florian.haftmann committed rISABELLE9017dfa56367: avoid _cmd suffix where no Isar command is involved.
avoid _cmd suffix where no Isar command is involved
Mon, Oct 12, 9:47 AM
florian.haftmann committed rISABELLEe1ee4a9902bd: centralized case distinction for beginning and ending nested targets in one….
centralized case distinction for beginning and ending nested targets in one…
Mon, Oct 12, 9:47 AM
florian.haftmann committed rAFP850e7a5db389: adjusted to changes in distribution.
adjusted to changes in distribution
Mon, Oct 12, 9:47 AM
florian.haftmann committed rAFPb2c51ec49da3: replaced combinators by more conventional nesting pattern.
replaced combinators by more conventional nesting pattern
Mon, Oct 12, 9:47 AM
florian.haftmann committed rAFP26c379b50c80: consolidated names and operations.
consolidated names and operations
Mon, Oct 12, 9:47 AM

Sun, Oct 11

florian.haftmann committed rISABELLEd62d84634b06: direct exit to theory when ending nested target on theory target.
direct exit to theory when ending nested target on theory target
Sun, Oct 11, 7:52 AM
florian.haftmann committed rISABELLE166fc8b9b4cd: tuned.
tuned
Sun, Oct 11, 7:52 AM
florian.haftmann committed rISABELLEcc27cf7e51c6: consolidated terminology.
consolidated terminology
Sun, Oct 11, 7:52 AM
florian.haftmann committed rISABELLE7e0e497dacbc: avoid baroque export.
avoid baroque export
Sun, Oct 11, 7:52 AM

Thu, Oct 8

florian.haftmann committed rAFP4fdf317282e9: typo.
typo
Thu, Oct 8, 4:28 PM
florian.haftmann committed rAFP7a6d65e5faef: factored out bit comprehension.
factored out bit comprehension
Thu, Oct 8, 11:33 AM
florian.haftmann committed rISABELLE48013583e8e6: factored out bit comprehension.
factored out bit comprehension
Thu, Oct 8, 11:33 AM

Wed, Oct 7

florian.haftmann committed rISABELLE633d14bd1e59: consolidated for the sake of documentation.
consolidated for the sake of documentation
Wed, Oct 7, 3:22 PM
florian.haftmann committed rAFPba6ffe9f3597: a small guide.
a small guide
Wed, Oct 7, 3:22 PM

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

Sep 17 2020

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

Sep 8 2020

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

Sep 7 2020

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

Sep 5 2020

florian.haftmann committed rISABELLE5a6d8675bf4b: generalized signed_take_bit.
generalized signed_take_bit
Sep 5 2020, 7:28 PM
florian.haftmann committed rISABELLEbb88e31220af: more on conversions.
more on conversions
Sep 5 2020, 7:28 PM
florian.haftmann committed rISABELLE12e94c2ff6c5: generalized.
generalized
Sep 5 2020, 7:28 PM
florian.haftmann committed rAFP21bc345f5a27: generalized signed_take_bit.
generalized signed_take_bit
Sep 5 2020, 7:27 PM
florian.haftmann committed rAFP3c01c6d69e78: more on conversions.
more on conversions
Sep 5 2020, 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