Page MenuHomeIsabelle/Phabricator

florian.haftmann (Florian Haftmann)
User

Projects

User Details

User Since
Nov 30 2019, 9:26 AM (66 w, 8 h)

Recent Activity

Yesterday

florian.haftmann committed rISABELLE10f5f5b880f4: typo.
typo
Fri, Mar 5, 11:00 AM

Tue, Mar 2

florian.haftmann committed rAFP0cbb56f4445a: reduced dependencies on theory List_Permutation.
reduced dependencies on theory List_Permutation
Tue, Mar 2, 4:32 PM
florian.haftmann committed rISABELLE649316106b08: reduced dependencies on theory List_Permutation.
reduced dependencies on theory List_Permutation
Tue, Mar 2, 4:32 PM

Mon, Mar 1

florian.haftmann committed rAFP7281051707f6: lemma diffusion.
lemma diffusion
Mon, Mar 1, 8:20 AM
florian.haftmann committed rAFP713ce6d3becb: dissolve theory with duplicated name from afp.
dissolve theory with duplicated name from afp
Mon, Mar 1, 8:20 AM
florian.haftmann committed rAFPa41a4c9f031d: more connections between mset _ = mset _ and permutations.
more connections between mset _ = mset _ and permutations
Mon, Mar 1, 8:20 AM
florian.haftmann committed rISABELLE2aef2de6b17c: NEWS.
NEWS
Mon, Mar 1, 8:16 AM
florian.haftmann committed rISABELLEff24fe85ee57: lemma diffusion.
lemma diffusion
Mon, Mar 1, 8:14 AM
florian.haftmann committed rISABELLEfd32f08f4fb5: more connections between mset _ = mset _ and permutations.
more connections between mset _ = mset _ and permutations
Mon, Mar 1, 8:14 AM
florian.haftmann committed rISABELLE7a88313895d5: dissolve theory with duplicated name from afp.
dissolve theory with duplicated name from afp
Mon, Mar 1, 8:14 AM

Thu, Feb 25

florian.haftmann committed rISABELLE95937cfe2628: merged.
merged
Thu, Feb 25, 3:54 PM
florian.haftmann committed rISABELLE47616dc81488: repaired document.
repaired document
Thu, Feb 25, 3:54 PM

Wed, Feb 24

florian.haftmann committed rAFPf7efb0c6c76f: emphasize connection to multisets.
emphasize connection to multisets
Wed, Feb 24, 7:13 PM
florian.haftmann committed rAFP6137b578dc54: multiset as equivalence class of permuted lists.
multiset as equivalence class of permuted lists
Wed, Feb 24, 7:13 PM
florian.haftmann committed rISABELLEbfe92e4f6ea4: multiset as equivalence class of permuted lists.
multiset as equivalence class of permuted lists
Wed, Feb 24, 7:12 PM
florian.haftmann committed rISABELLEc52c5a5bf4e6: emphasize connection to multisets.
emphasize connection to multisets
Wed, Feb 24, 7:12 PM

Tue, Feb 23

florian.haftmann committed rAFP5c7a3b0533b3: more specific name.
more specific name
Tue, Feb 23, 10:04 PM
florian.haftmann committed rISABELLEbeaff25452d2: more specific name.
more specific name
Tue, Feb 23, 10:03 PM
florian.haftmann committed rISABELLE2ac92ba88d6b: more lemmas.
more lemmas
Tue, Feb 23, 10:03 PM
florian.haftmann committed rISABELLE6c4c37a3ebec: dropped obscure FIXME.
dropped obscure FIXME
Tue, Feb 23, 10:03 PM

Mon, Feb 22

florian.haftmann committed rISABELLEce4fe0b1cfda: NEWS.
NEWS
Mon, Feb 22, 7:31 PM
florian.haftmann committed rISABELLEe2d03448d5b5: get rid of traditional predicate.
get rid of traditional predicate
Mon, Feb 22, 7:31 PM
florian.haftmann committed rISABELLE05a873f90655: dedicated locale for preorder and abstract bdd operation.
dedicated locale for preorder and abstract bdd operation
Mon, Feb 22, 7:31 PM
florian.haftmann committed rAFP908f7c03d556: get rid of traditional predicate.
get rid of traditional predicate
Mon, Feb 22, 7:30 PM
florian.haftmann committed rAFPf8f24482ab45: dedicated locale for preorder and abstract bdd operation.
dedicated locale for preorder and abstract bdd operation
Mon, Feb 22, 7:30 PM

Jan 7 2021

florian.haftmann committed rISABELLEdc62ecc7e59a: dropped junk.
dropped junk
Jan 7 2021, 10:23 AM

Dec 20 2020

florian.haftmann committed rAFP729b746aa6d5: more precise simpset for method unat_arith.
more precise simpset for method unat_arith
Dec 20 2020, 11:01 AM
florian.haftmann committed rISABELLEeb1e5c4f70cd: more precise simpset for method unat_arith.
more precise simpset for method unat_arith
Dec 20 2020, 11:01 AM

Dec 19 2020

florian.haftmann committed rISABELLE90ada01470cb: clarified scope of concept.
clarified scope of concept
Dec 19 2020, 3:20 PM
florian.haftmann committed rISABELLE09479be1fe2a: clarified name.
clarified name
Dec 19 2020, 10:32 AM

Dec 7 2020

florian.haftmann committed rAFP77790ea69409: avoid generated code in versioning -- ONLY PARTIALLY TESTED DUE TO NON-SELF….
avoid generated code in versioning -- ONLY PARTIALLY TESTED DUE TO NON-SELF…
Dec 7 2020, 11:28 AM

Dec 6 2020

florian.haftmann committed rAFPaf0298e0b819: moved some lemmas from AFP to distribution.
moved some lemmas from AFP to distribution
Dec 6 2020, 8:25 AM
florian.haftmann committed rISABELLEec0d3a62bb3b: moved some lemmas from AFP to distribution.
moved some lemmas from AFP to distribution
Dec 6 2020, 8:24 AM

Dec 5 2020

florian.haftmann committed rAFP59470eb9f5ab: sorted out lemmas.
sorted out lemmas
Dec 5 2020, 11:12 AM

Nov 29 2020

florian.haftmann committed rISABELLE4dcd05a26795: typo.
typo
Nov 29 2020, 4:38 PM
florian.haftmann committed rISABELLE4ab04bafae35: more on signed division.
more on signed division
Nov 29 2020, 4:38 PM
florian.haftmann committed rAFP009fa5ffc3e6: sorted out lemmas.
sorted out lemmas
Nov 29 2020, 4:37 PM

Nov 27 2020

florian.haftmann committed rAFPa13bec92d3d2: opening is now a keyword.
opening is now a keyword
Nov 27 2020, 1:03 PM
florian.haftmann committed rAFP69f3a2dbc505: sorted out lemmas.
sorted out lemmas
Nov 27 2020, 1:03 PM
florian.haftmann committed rISABELLEe7c2848b78e8: refined syntax for bundle mixins for locale and class specifications.
refined syntax for bundle mixins for locale and class specifications
Nov 27 2020, 1:02 PM

Nov 23 2020

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

Nov 22 2020

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

Nov 20 2020

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

Nov 19 2020

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

Nov 16 2020

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

Nov 15 2020

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

Nov 12 2020

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

Nov 6 2020

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

Nov 5 2020

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

Nov 4 2020

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

Nov 1 2020

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

Oct 30 2020

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

Oct 29 2020

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
Oct 29 2020, 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
Oct 29 2020, 1:58 PM
florian.haftmann committed rISABELLEd8661799afb2: removed dependency.
removed dependency
Oct 29 2020, 1:58 PM

Oct 28 2020

florian.haftmann committed rAFPede4399b471c: more lemmas.
more lemmas
Oct 28 2020, 7:43 AM
florian.haftmann committed rISABELLE83b5911c0164: more lemmas.
more lemmas
Oct 28 2020, 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