Page MenuHomeIsabelle/Phabricator

florian.haftmann (Florian Haftmann)
User

Projects

User Details

User Since
Nov 30 2019, 9:26 AM (35 w, 6 d)

Recent Activity

Yesterday

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

Wed, Aug 5

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

Tue, Aug 4

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

Sat, Aug 1

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

Thu, Jul 16

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

Mon, Jul 13

florian.haftmann committed rISABELLE08f1e4cb735f: concatentation of bit values.
concatentation of bit values
Mon, Jul 13, 7:25 PM
florian.haftmann committed rAFPce2c72a0a05e: concatentation of bit values.
concatentation of bit values
Mon, Jul 13, 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…
Mon, Jul 13, 8:08 AM
florian.haftmann committed rISABELLE5689f0db4508: more simp rules for concrete numerical values.
more simp rules for concrete numerical values
Mon, Jul 13, 8:08 AM
florian.haftmann committed rISABELLEb4ed07cbe954: words added to code generator test.
words added to code generator test
Mon, Jul 13, 8:08 AM
florian.haftmann committed rAFP7b844df07b1c: prefer canonically oriented lists of bits in definitions.
prefer canonically oriented lists of bits in definitions
Mon, Jul 13, 8:07 AM

Sat, Jul 11

florian.haftmann committed rISABELLE9b4135e8bade: a generic horner sum operation.
a generic horner sum operation
Sat, Jul 11, 11:17 PM
florian.haftmann committed rISABELLE08348e364739: more thms.
more thms
Sat, Jul 11, 11:17 PM
florian.haftmann committed rISABELLEfebdd4eead56: more on single-bit operations.
more on single-bit operations
Sat, Jul 11, 9:15 AM
florian.haftmann committed rISABELLEa851ce626b78: signed_take_bit.
signed_take_bit
Sat, Jul 11, 9:15 AM
florian.haftmann committed rAFP70ae335403b7: signed_take_bit.
signed_take_bit
Sat, Jul 11, 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
florian.haftmann committed rISABELLE428609096812: more lemmas and less name space pollution.
more lemmas and less name space pollution
Jun 18 2020, 7:15 PM
florian.haftmann committed rISABELLE2efc5b8c7456: 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:15 PM
florian.haftmann committed rISABELLEac6f9738c200: essential instance about bit structure.
essential instance about bit structure
Jun 18 2020, 7:15 PM
florian.haftmann committed rISABELLEc9251bc7da4e: more transfer rules.
more transfer rules
Jun 18 2020, 7:15 PM
florian.haftmann committed rISABELLE6ede899d26d3: fundamental construction of word type following existing transfer rules.
fundamental construction of word type following existing transfer rules
Jun 18 2020, 7:15 PM
florian.haftmann committed rISABELLE5b8b1183c641: dropped yet another duplicate.
dropped yet another duplicate
Jun 18 2020, 7:15 PM
florian.haftmann committed rISABELLE476b9e6904d9: replaced mere alias by input abbreviation.
replaced mere alias by input abbreviation
Jun 18 2020, 7:15 PM
florian.haftmann committed rISABELLE4b1264316270: replaced operation with weak abstraction by input abbreviation.
replaced operation with weak abstraction by input abbreviation
Jun 18 2020, 7:14 PM
florian.haftmann committed rISABELLE4d4079159be7: replaced mere alias by abbreviation.
replaced mere alias by abbreviation
Jun 18 2020, 7:14 PM
florian.haftmann committed rISABELLE18357df1cd20: avoid compound operation.
avoid compound operation
Jun 18 2020, 7:14 PM
florian.haftmann committed rISABELLEd3fb19847662: formal relationships between operations.
formal relationships between operations
Jun 18 2020, 7:14 PM
florian.haftmann committed rISABELLEd2654b30f7bd: eliminated warnings.
eliminated warnings
Jun 18 2020, 7:14 PM
florian.haftmann committed rISABELLE49af3d9a818c: replaced mere alias by input abbreviation.
replaced mere alias by input abbreviation
Jun 18 2020, 7:14 PM

Jun 16 2020

florian.haftmann committed rISABELLEe1b262e7480c: interpretations for boolean operators.
interpretations for boolean operators
Jun 16 2020, 12:09 PM
florian.haftmann committed rISABELLE92de7d74b8f8: more specific thm reference.
more specific thm reference
Jun 16 2020, 12:09 PM
florian.haftmann committed rAFP78141c8a7974: interpretations for boolean operators.
interpretations for boolean operators
Jun 16 2020, 12:04 PM

Jun 6 2020

florian.haftmann committed rISABELLE7b34a932eeb6: NEWS.
NEWS
Jun 6 2020, 11:01 AM

Jun 5 2020

florian.haftmann committed rISABELLE2c6a5c709f22: more theorems.
more theorems
Jun 5 2020, 7:12 AM
florian.haftmann committed rISABELLEa238074c5a9d: avoid overaggressive default simp rules.
avoid overaggressive default simp rules
Jun 5 2020, 7:12 AM

Jun 4 2020

florian.haftmann committed rISABELLEb0da0537f307: activate simproc for FOL.
activate simproc for FOL
Jun 4 2020, 5:40 PM
florian.haftmann committed rISABELLE2e7df6774373: more rules for FOL also.
more rules for FOL also
Jun 4 2020, 5:40 PM
florian.haftmann committed rISABELLE4e0a58818edc: more simp rules.
more simp rules
Jun 4 2020, 5:40 PM
florian.haftmann committed rAFP4d493338c3a7: activate simproc for FOL.
activate simproc for FOL
Jun 4 2020, 5:40 PM
florian.haftmann committed rAFP2f1b5352ff77: more rules for FOL also.
more rules for FOL also
Jun 4 2020, 5:39 PM
florian.haftmann committed rAFPcce073a27f08: more simp rules.
more simp rules
Jun 4 2020, 5:39 PM

May 30 2020

florian.haftmann committed rISABELLE435cdc772110: specific atomization inert to later rule set modifications.
specific atomization inert to later rule set modifications
May 30 2020, 8:07 PM
florian.haftmann committed rISABELLE3956d85e8e81: more precise scope of atomize.
more precise scope of atomize
May 30 2020, 8:07 PM
florian.haftmann committed rISABELLE3867734b9a40: install simproc but deactivate by default.
install simproc but deactivate by default
May 30 2020, 1:49 PM

May 25 2020

florian.haftmann committed rISABELLE4f4695757980: better closeup and more consistent terminology.
better closeup and more consistent terminology
May 25 2020, 7:45 AM

May 22 2020

florian.haftmann committed rISABELLE6a51e64ba13d: slightly more specific implementations.
slightly more specific implementations
May 22 2020, 6:29 AM
florian.haftmann committed rISABELLE30d92e668b52: tuned module name space for generated code.
tuned module name space for generated code
May 22 2020, 6:29 AM

May 21 2020

florian.haftmann committed rISABELLE34ecb540a079: generalized and augmented.
generalized and augmented
May 21 2020, 11:04 AM

May 20 2020

florian.haftmann committed rISABELLEda12452c9be2: corrected spelling and tuned whitespace.
corrected spelling and tuned whitespace
May 20 2020, 8:35 AM

May 9 2020

florian.haftmann committed rISABELLEf424e164d752: modernized notation for bit operations.
modernized notation for bit operations
May 9 2020, 7:34 PM
florian.haftmann committed rAFPe3d9183d726a: modernized notation for bit operations.
modernized notation for bit operations
May 9 2020, 7:33 PM