Page MenuHomeIsabelle/Phabricator

florian.haftmann (Florian Haftmann)
User

Projects

User Details

User Since
Nov 30 2019, 9:26 AM (80 w, 1 d)

Recent Activity

Thu, Jun 10

florian.haftmann committed rISABELLEbfce186331be: more succint interfaces.
more succint interfaces
Thu, Jun 10, 9:08 AM
florian.haftmann committed rISABELLE9447668d1b77: global interpretation into nested targets.
global interpretation into nested targets
Thu, Jun 10, 9:08 AM

Sun, Jun 6

florian.haftmann committed rISABELLE0510c7a4256a: moved more legacy to AFP.
moved more legacy to AFP
Sun, Jun 6, 7:01 PM
florian.haftmann committed rAFP0b37c282b057: moved more legacy to AFP.
moved more legacy to AFP
Sun, Jun 6, 7:00 PM

Thu, Jun 3

florian.haftmann committed rAFPe2811dc54d05: grouped lemmas.
grouped lemmas
Thu, Jun 3, 8:25 AM
florian.haftmann committed rISABELLEe75635a0bafd: lexorders the locale way.
lexorders the locale way
Thu, Jun 3, 8:05 AM

Wed, Jun 2

florian.haftmann committed rISABELLE26c0ccf17f31: more accurate export morphism enables proper instantiation by interpretation.
more accurate export morphism enables proper instantiation by interpretation
Wed, Jun 2, 5:22 PM

Sun, May 30

florian.haftmann committed rAFPfd98855f4f8e: bundles for traditional infix syntax.
bundles for traditional infix syntax
Sun, May 30, 8:55 AM

Sat, May 29

florian.haftmann committed rISABELLEaab7975fa070: more lemmas.
more lemmas
Sat, May 29, 7:59 AM
florian.haftmann committed rISABELLE35217bf33215: max word moved to Word_Lib in AFP.
max word moved to Word_Lib in AFP
Sat, May 29, 7:59 AM
florian.haftmann committed rAFPbdcaff25a220: complement reduced to mere abbreviation.
complement reduced to mere abbreviation
Sat, May 29, 7:59 AM
florian.haftmann committed rAFP3ddc21f61385: max word moved to Word_Lib in AFP.
max word moved to Word_Lib in AFP
Sat, May 29, 7:59 AM
florian.haftmann committed rAFPd7c3c888a331: extracted more legacy abbreviations.
extracted more legacy abbreviations
Sat, May 29, 7:59 AM

Thu, May 27

florian.haftmann committed rAFP7c0105d2d63f: tuned presentation.
tuned presentation
Thu, May 27, 11:31 PM
florian.haftmann committed rAFPd92f99905ee2: adjusted to changes in distribution.
adjusted to changes in distribution
Thu, May 27, 11:31 PM
florian.haftmann committed rAFP97869e45578a: adjusted to change in distribution.
adjusted to change in distribution
Thu, May 27, 11:31 PM

Mon, May 17

florian.haftmann committed rAFPe766628a0795: mere abbreviation for logical alias.
mere abbreviation for logical alias
Mon, May 17, 12:33 PM
florian.haftmann committed rISABELLE4b1386b2c23e: mere abbreviation for logical alias.
mere abbreviation for logical alias
Mon, May 17, 12:32 PM

May 13 2021

florian.haftmann committed rISABELLE78044b2f001c: explicit type class operations for type-specific implementations.
explicit type class operations for type-specific implementations
May 13 2021, 11:25 AM
florian.haftmann committed rISABELLE3708884bfa8a: obsolete.
obsolete
May 13 2021, 11:25 AM
florian.haftmann committed rAFPa19043a5f828: explicit type class operations for type-specific implementations.
explicit type class operations for type-specific implementations
May 13 2021, 11:25 AM
florian.haftmann committed rAFPa055a33fcb58: next step to phase out ancient numerals.
next step to phase out ancient numerals
May 13 2021, 11:25 AM

May 11 2021

florian.haftmann committed rAFP0ace227c4d10: centralized more lemmas.
centralized more lemmas
May 11 2021, 1:30 PM
florian.haftmann committed rAFPaac14245270a: avoid Fun.swap.
avoid Fun.swap
May 11 2021, 1:30 PM
florian.haftmann committed rAFP3945ab3f00b8: guide is out of focus.
guide is out of focus
May 11 2021, 1:30 PM
florian.haftmann committed rISABELLE7734c442802f: avoid Fun.swap.
avoid Fun.swap
May 11 2021, 1:30 PM
florian.haftmann committed rISABELLE6e26d06b24b1: centralized more lemmas.
centralized more lemmas
May 11 2021, 1:30 PM
florian.haftmann committed rISABELLEfecfb96474ca: guide is out of focus.
guide is out of focus
May 11 2021, 1:30 PM

May 9 2021

florian.haftmann committed rISABELLE1bd3463e30b8: more elementary swap.
more elementary swap
May 9 2021, 8:36 AM
florian.haftmann committed rAFPf8ded3c69c5d: more elementary swap.
more elementary swap
May 9 2021, 8:34 AM

May 5 2021

florian.haftmann committed rISABELLE5020054b3a16: tuned theory structure.
tuned theory structure
May 5 2021, 6:19 PM
florian.haftmann committed rISABELLE4dc3baf45d6a: more appropriate location.
more appropriate location
May 5 2021, 6:19 PM
florian.haftmann committed rAFPf9dd3b4a6fd5: tuned theory structure.
tuned theory structure
May 5 2021, 6:18 PM
florian.haftmann committed rISABELLEb4b70d13c995: collected lemmas on permutations.
collected lemmas on permutations
May 5 2021, 7:28 AM
florian.haftmann committed rAFP6cf5bfc61f4b: collected lemmas on permutations.
collected lemmas on permutations
May 5 2021, 7:26 AM

Apr 23 2021

florian.haftmann committed rAFP28fe4ca859cd: collecting more lemmas concerning multisets.
collecting more lemmas concerning multisets
Apr 23 2021, 2:43 PM
florian.haftmann committed rISABELLE5c4a09c4bc9c: collecting more lemmas concerning multisets.
collecting more lemmas concerning multisets
Apr 23 2021, 2:42 PM

Apr 16 2021

florian.haftmann committed rISABELLEed5226fdf89d: proper context variable handling when stripping leadings quantifiers from test….
proper context variable handling when stripping leadings quantifiers from test…
Apr 16 2021, 7:26 AM

Apr 11 2021

florian.haftmann committed rAFPbf1f2a489b41: collected combinatorial material.
collected combinatorial material
Apr 11 2021, 9:45 AM
florian.haftmann committed rISABELLE92783562ab78: collected combinatorial material.
collected combinatorial material
Apr 11 2021, 9:42 AM

Apr 8 2021

florian.haftmann committed rAFPc351b9b63b58: confluent preprocessing for floats in presence of target language numerals.
confluent preprocessing for floats in presence of target language numerals
Apr 8 2021, 4:30 PM
florian.haftmann committed rISABELLE7cb3fefef79e: confluent preprocessing for floats in presence of target language numerals.
confluent preprocessing for floats in presence of target language numerals
Apr 8 2021, 4:30 PM
florian.haftmann committed rISABELLEfc72e5ebf9de: subclass relation.
subclass relation
Apr 8 2021, 2:23 PM
florian.haftmann committed rAFPb3ff22dfc82d: subclass relation.
subclass relation
Apr 8 2021, 2:22 PM

Apr 7 2021

florian.haftmann committed rISABELLE5131c388a9b0: simplified definition.
simplified definition
Apr 7 2021, 5:02 PM
florian.haftmann committed rAFPeb11506f9cf9: simplified definition.
simplified definition
Apr 7 2021, 5:02 PM

Apr 6 2021

florian.haftmann committed rISABELLE0f33c7031ec9: new lemmas.
new lemmas
Apr 6 2021, 8:39 PM
florian.haftmann committed rAFP63ca4e334ffc: new lemmas.
new lemmas
Apr 6 2021, 8:38 PM

Mar 25 2021

florian.haftmann committed rAFP46026e61801e: dedicated session for combinatorial material.
dedicated session for combinatorial material
Mar 25 2021, 10:25 AM
florian.haftmann committed rISABELLE1d8a79aa2a99: dedicated session for combinatorial material.
dedicated session for combinatorial material
Mar 25 2021, 10:23 AM

Mar 22 2021

florian.haftmann committed rAFP184d9cadd5ca: more lemmas.
more lemmas
Mar 22 2021, 12:55 PM
florian.haftmann committed rISABELLEee1c4962671c: more lemmas.
more lemmas
Mar 22 2021, 12:54 PM

Mar 18 2021

florian.haftmann committed rISABELLE99950990c7b3: prefer more direct interpretation.
prefer more direct interpretation
Mar 18 2021, 7:32 PM

Mar 11 2021

florian.haftmann committed rAFP1335f4299090: avoid name clash.
avoid name clash
Mar 11 2021, 11:57 AM
florian.haftmann committed rISABELLE1f1366966296: avoid name clash.
avoid name clash
Mar 11 2021, 11:57 AM
florian.haftmann committed rISABELLE7b59d2945e54: lemma.
lemma
Mar 11 2021, 11:57 AM

Mar 8 2021

florian.haftmann committed rISABELLE6a96e9406e53: reduced dependencies on List_Permutation.
reduced dependencies on List_Permutation
Mar 8 2021, 8:25 AM
florian.haftmann committed rISABELLE2e6b2134956e: follow corresponding precedence on sets.
follow corresponding precedence on sets
Mar 8 2021, 8:25 AM
florian.haftmann committed rAFP2961a61999bd: reduced dependencies on List_Permutation.
reduced dependencies on List_Permutation
Mar 8 2021, 8:23 AM
florian.haftmann committed rAFP18cd8aa0ceae: follow corresponding precedence on sets.
follow corresponding precedence on sets
Mar 8 2021, 8:23 AM

Mar 6 2021

florian.haftmann committed rISABELLE716d256259d5: consolidated names.
consolidated names
Mar 6 2021, 10:30 PM
florian.haftmann committed rISABELLE24f0df084aad: reduced dependencies on theory List_Permutation.
reduced dependencies on theory List_Permutation
Mar 6 2021, 10:30 PM
florian.haftmann committed rAFP48319c117066: consolidated names.
consolidated names
Mar 6 2021, 10:29 PM
florian.haftmann committed rAFPb6ad06ee02b5: reduced dependencies on theory List_Permutation.
reduced dependencies on theory List_Permutation
Mar 6 2021, 10:29 PM

Mar 5 2021

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

Mar 2 2021

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

Mar 1 2021

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

Feb 25 2021

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

Feb 24 2021

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

Feb 23 2021

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

Feb 22 2021

florian.haftmann committed rISABELLEce4fe0b1cfda: NEWS.
NEWS
Feb 22 2021, 7:31 PM
florian.haftmann committed rISABELLEe2d03448d5b5: get rid of traditional predicate.
get rid of traditional predicate
Feb 22 2021, 7:31 PM
florian.haftmann committed rISABELLE05a873f90655: dedicated locale for preorder and abstract bdd operation.
dedicated locale for preorder and abstract bdd operation
Feb 22 2021, 7:31 PM
florian.haftmann committed rAFP908f7c03d556: get rid of traditional predicate.
get rid of traditional predicate
Feb 22 2021, 7:30 PM
florian.haftmann committed rAFPf8f24482ab45: dedicated locale for preorder and abstract bdd operation.
dedicated locale for preorder and abstract bdd operation
Feb 22 2021, 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