Page MenuHomeIsabelle/Phabricator

florian.haftmann (Florian Haftmann)
User

Projects

User Details

User Since
Nov 30 2019, 9:26 AM (51 w, 5 d)

Recent Activity

Mon, Nov 23

florian.haftmann committed rAFP348d64d3a54d: sorted out lemmas.
sorted out lemmas
Mon, Nov 23, 3:40 PM

Sun, Nov 22

florian.haftmann committed rAFP5ded4ffd242b: sorted out lemmas.
sorted out lemmas
Sun, Nov 22, 6:06 PM
florian.haftmann committed rAFP38e989792057: sorted out lemmas.
sorted out lemmas
Sun, Nov 22, 6:06 PM
florian.haftmann committed rAFPc7ce9d354883: sorted out lemmas.
sorted out lemmas
Sun, Nov 22, 7:40 AM

Fri, Nov 20

florian.haftmann committed rAFP13c18a730ac4: factored out lemmas.
factored out lemmas
Fri, Nov 20, 3:17 PM

Thu, Nov 19

florian.haftmann committed rAFPd6be5fd1a75a: factored out operations.
factored out operations
Thu, Nov 19, 6:17 PM
florian.haftmann committed rAFPd70a12cf43c4: collected and streamlined some auxiliary.
collected and streamlined some auxiliary
Thu, Nov 19, 3:48 PM
florian.haftmann committed rAFP3b3d09186d48: more collecting and grouping of lemmas.
more collecting and grouping of lemmas
Thu, Nov 19, 3:48 PM
florian.haftmann committed rAFP21e7ccd3d91a: guide.
guide
Thu, Nov 19, 3:48 PM

Mon, Nov 16

florian.haftmann committed rISABELLE4b2691211719: moved lemmas from AFP to distribution.
moved lemmas from AFP to distribution
Mon, Nov 16, 7:32 AM
florian.haftmann committed rAFP6e1edf05bf99: moved lemmas from AFP to distribution.
moved lemmas from AFP to distribution
Mon, Nov 16, 7:31 AM

Sun, Nov 15

florian.haftmann committed rISABELLEc7bc3e70a8c7: official collection for bit projection simplifications.
official collection for bit projection simplifications
Sun, Nov 15, 5:52 PM
florian.haftmann committed rAFPcbfcaad565f1: official collection for bit projection simplifications.
official collection for bit projection simplifications
Sun, Nov 15, 5:51 PM
florian.haftmann committed rAFPb41e4757c02f: bundles for reflected term syntax.
bundles for reflected term syntax
Sun, Nov 15, 10:55 AM
florian.haftmann committed rISABELLEe7ee815b04bf: CONTRIBUTORS.
CONTRIBUTORS
Sun, Nov 15, 10:53 AM
florian.haftmann committed rISABELLEfeebdaa346e5: bundles for reflected term syntax.
bundles for reflected term syntax
Sun, Nov 15, 10:53 AM
florian.haftmann committed rISABELLEa4cb880e873a: type alias for mixin bundles.
type alias for mixin bundles
Sun, Nov 15, 10:53 AM

Thu, Nov 12

florian.haftmann committed rAFP3b0a53813ac2: bundled syntax for state monad combinators.
bundled syntax for state monad combinators
Thu, Nov 12, 9:08 AM
florian.haftmann committed rISABELLEde581f98a3a1: bundled syntax for state monad combinators.
bundled syntax for state monad combinators
Thu, Nov 12, 9:07 AM

Fri, Nov 6

florian.haftmann committed rAFPc8d4f20a1071: dedicated integration theory for word8/16/32/64.
dedicated integration theory for word8/16/32/64
Fri, Nov 6, 5:06 PM

Thu, Nov 5

florian.haftmann committed rAFP375469c07787: further decomposition.
further decomposition
Thu, Nov 5, 12:58 PM

Wed, Nov 4

florian.haftmann committed rAFP6da5282d3ddb: streamlined auxiliary theories.
streamlined auxiliary theories
Wed, Nov 4, 8:44 PM
florian.haftmann committed rAFP5456b058dbbf: tuned structure formally.
tuned structure formally
Wed, Nov 4, 8:53 AM
florian.haftmann committed rISABELLE58b1826354c9: NEWS and CONTRIBUTORS.
NEWS and CONTRIBUTORS
Wed, Nov 4, 8:51 AM

Sun, Nov 1

florian.haftmann committed rAFP82f18c28f31b: adjusted to distribution.
adjusted to distribution
Sun, Nov 1, 5:28 PM
florian.haftmann committed rISABELLE589645894305: bundle mixins for locale and class specifications.
bundle mixins for locale and class specifications
Sun, Nov 1, 5:27 PM

Fri, Oct 30

florian.haftmann committed rISABELLEc2b643c9f2bf: unified slots.
unified slots
Fri, Oct 30, 8:02 AM
florian.haftmann committed rISABELLE17dc99589a91: unified Local_Theory.init with Generic_Target.init.
unified Local_Theory.init with Generic_Target.init
Fri, Oct 30, 8:02 AM

Thu, Oct 29

florian.haftmann committed rAFP1d9680ca2b5c: moved most material from session HOL-Word to Word_Lib in the AFP.
moved most material from session HOL-Word to Word_Lib in the AFP
Thu, Oct 29, 2:01 PM
florian.haftmann committed rISABELLEc7038c397ae3: moved most material from session HOL-Word to Word_Lib in the AFP.
moved most material from session HOL-Word to Word_Lib in the AFP
Thu, Oct 29, 1:58 PM
florian.haftmann committed rISABELLEd8661799afb2: removed dependency.
removed dependency
Thu, Oct 29, 1:58 PM

Wed, Oct 28

florian.haftmann committed rAFPede4399b471c: more lemmas.
more lemmas
Wed, Oct 28, 7:43 AM
florian.haftmann committed rISABELLE83b5911c0164: more lemmas.
more lemmas
Wed, Oct 28, 7:42 AM

Oct 26 2020

florian.haftmann committed rAFP4531dd70c28b: factored out theory Traditional_Syntax.
factored out theory Traditional_Syntax
Oct 26 2020, 12:47 PM
florian.haftmann committed rISABELLEc89d8e8bd8c7: factored out theory Traditional_Syntax.
factored out theory Traditional_Syntax
Oct 26 2020, 12:46 PM

Oct 24 2020

florian.haftmann committed rISABELLE974071d873ba: tuned interfaces.
tuned interfaces
Oct 24 2020, 9:35 PM
florian.haftmann committed rISABELLE13032e920fea: tuned.
tuned
Oct 24 2020, 9:35 PM

Oct 23 2020

florian.haftmann committed rAFP86066860b37d: enforce strict nesting of local theories.
enforce strict nesting of local theories
Oct 23 2020, 9:21 AM
florian.haftmann committed rISABELLEff181cd78bb7: enforce strict nesting of local theories.
enforce strict nesting of local theories
Oct 23 2020, 9:11 AM

Oct 17 2020

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

Oct 12 2020

florian.haftmann committed rISABELLEe4dde7beab39: dedicated module for toplevel target handling.
dedicated module for toplevel target handling
Oct 12 2020, 9:47 AM
florian.haftmann committed rISABELLE24bd1316eaae: consolidated names and operations.
consolidated names and operations
Oct 12 2020, 9:47 AM
florian.haftmann committed rISABELLEe51f1733618d: replaced combinators by more conventional nesting pattern.
replaced combinators by more conventional nesting pattern
Oct 12 2020, 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
Oct 12 2020, 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…
Oct 12 2020, 9:47 AM
florian.haftmann committed rAFP850e7a5db389: adjusted to changes in distribution.
adjusted to changes in distribution
Oct 12 2020, 9:47 AM
florian.haftmann committed rAFPb2c51ec49da3: replaced combinators by more conventional nesting pattern.
replaced combinators by more conventional nesting pattern
Oct 12 2020, 9:47 AM
florian.haftmann committed rAFP26c379b50c80: consolidated names and operations.
consolidated names and operations
Oct 12 2020, 9:47 AM

Oct 11 2020

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
Oct 11 2020, 7:52 AM
florian.haftmann committed rISABELLE166fc8b9b4cd: tuned.
tuned
Oct 11 2020, 7:52 AM
florian.haftmann committed rISABELLEcc27cf7e51c6: consolidated terminology.
consolidated terminology
Oct 11 2020, 7:52 AM
florian.haftmann committed rISABELLE7e0e497dacbc: avoid baroque export.
avoid baroque export
Oct 11 2020, 7:52 AM

Oct 8 2020

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

Oct 7 2020

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

Sep 25 2020

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

Sep 23 2020

florian.haftmann committed rAFPf04759177a5d: canonical enum instance for word.
canonical enum instance for word
Sep 23 2020, 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…
Sep 23 2020, 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…
Sep 23 2020, 1:18 PM
florian.haftmann committed rISABELLEdb43ee05066d: canonical enum instance for word.
canonical enum instance for word
Sep 23 2020, 1:18 PM

Sep 20 2020

florian.haftmann committed rAFPb3e61e86eff9: identified operation alias; tuned.
identified operation alias; tuned
Sep 20 2020, 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