Page MenuHomeIsabelle/Phabricator

florian.haftmann (Florian Haftmann)
User

Projects

User Details

User Since
Nov 30 2019, 9:26 AM (94 w, 3 d)

Recent Activity

Mon, Sep 13

florian.haftmann committed rAFP33b9d9a97696: explicit predicate for confined bit range avoids cyclic rewriting in presence….
explicit predicate for confined bit range avoids cyclic rewriting in presence…
Mon, Sep 13, 4:20 PM
florian.haftmann committed rISABELLE42523fbf643b: explicit predicate for confined bit range avoids cyclic rewriting in presence….
explicit predicate for confined bit range avoids cyclic rewriting in presence…
Mon, Sep 13, 4:19 PM

Aug 22 2021

florian.haftmann committed rISABELLEafe3c8ae1624: consolidation of rules for bit operations.
consolidation of rules for bit operations
Aug 22 2021, 7:59 AM
florian.haftmann committed rAFP897dc683c2ec: consolidation of rules for bit operations.
consolidation of rules for bit operations
Aug 22 2021, 7:56 AM

Aug 12 2021

florian.haftmann committed rAFPd8cd1583a4f6: repaired syntax.
repaired syntax
Aug 12 2021, 4:20 PM

Aug 5 2021

florian.haftmann committed rAFP393bd86c18ea: antiquotation for bundles.
antiquotation for bundles
Aug 5 2021, 9:22 AM
florian.haftmann committed rAFPd4adf5def3dd: clarified abstract and concrete boolean algebras.
clarified abstract and concrete boolean algebras
Aug 5 2021, 9:22 AM
florian.haftmann committed rISABELLE7c5842b06114: clarified abstract and concrete boolean algebras.
clarified abstract and concrete boolean algebras
Aug 5 2021, 9:21 AM
florian.haftmann committed rISABELLE7d3e818fe21f: antiquotation for bundles.
antiquotation for bundles
Aug 5 2021, 9:21 AM

Aug 3 2021

florian.haftmann committed rAFP13152a0c7b0c: simplified hierarchy of type classes for bit operations.
simplified hierarchy of type classes for bit operations
Aug 3 2021, 9:37 PM
florian.haftmann committed rISABELLE3146646a43a7: simplified hierarchy of type classes for bit operations.
simplified hierarchy of type classes for bit operations
Aug 3 2021, 9:36 PM
florian.haftmann committed rISABELLE2ab5dacdb1f6: obsolete.
obsolete
Aug 3 2021, 9:36 PM

Aug 2 2021

florian.haftmann committed rAFPda7fd1ac6b66: restored executable conversions.
restored executable conversions
Aug 2 2021, 6:11 PM
florian.haftmann committed rAFP7f4f3900fd58: dropped junk.
dropped junk
Aug 2 2021, 6:11 PM
florian.haftmann committed rISABELLEd804e93ae9ff: moved theory Bit_Operations into Main corpus.
moved theory Bit_Operations into Main corpus
Aug 2 2021, 12:07 PM
florian.haftmann committed rAFPc341fdde0cba: moved theory Bit_Operations into Main corpus.
moved theory Bit_Operations into Main corpus
Aug 2 2021, 12:07 PM

Aug 1 2021

florian.haftmann committed rISABELLE6d7be1227d02: organize syntax for word operations in bundles.
organize syntax for word operations in bundles
Aug 1 2021, 12:45 PM
florian.haftmann committed rAFPfc03e8f2954c: organize syntax for word operations in bundles.
organize syntax for word operations in bundles
Aug 1 2021, 12:44 PM

Jul 31 2021

florian.haftmann committed rAFP82cfa5e04c85: more systematic approach for instantiation.
more systematic approach for instantiation
Jul 31 2021, 6:08 PM
florian.haftmann committed rAFPf5bee47345aa: avoid seemingly unused transfer rules.
avoid seemingly unused transfer rules
Jul 31 2021, 6:08 PM

Jul 17 2021

florian.haftmann committed rISABELLE47a568d9067e: CONTRIBUTORS.
CONTRIBUTORS
Jul 17 2021, 10:58 AM

Jul 13 2021

florian.haftmann committed rAFP1ed4c9f5c24d: more coherent dependencies.
more coherent dependencies
Jul 13 2021, 7:38 AM

Jul 12 2021

florian.haftmann committed rISABELLEca2a35c0fe6e: operations for symbolic computation of bit operations.
operations for symbolic computation of bit operations
Jul 12 2021, 2:02 PM
florian.haftmann committed rISABELLE0274d442b7ea: proper local context.
proper local context
Jul 12 2021, 2:02 PM
florian.haftmann committed rAFPd77834415899: operations for symbolic computation of bit operations.
operations for symbolic computation of bit operations
Jul 12 2021, 2:00 PM

Jun 24 2021

florian.haftmann committed rAFP1a99ac2d4342: more word cleanup.
more word cleanup
Jun 24 2021, 1:31 PM
florian.haftmann committed rISABELLEf46e9f75b7d5: more word cleanup.
more word cleanup
Jun 24 2021, 1:30 PM

Jun 23 2021

florian.haftmann committed rISABELLE7181130f5872: more default simp rules.
more default simp rules
Jun 23 2021, 8:38 PM
florian.haftmann committed rISABELLEd156b141fe2f: merged.
merged
Jun 23 2021, 8:38 PM
florian.haftmann committed rISABELLE465846b611d5: some word streamlining.
some word streamlining
Jun 23 2021, 8:38 PM
florian.haftmann committed rAFPf1195cc96e85: more default simp rules.
more default simp rules
Jun 23 2021, 8:38 PM
florian.haftmann committed rAFP9e42e0c5f9f9: some word streamlining.
some word streamlining
Jun 23 2021, 8:38 PM

Jun 22 2021

florian.haftmann committed rAFP55af834ad1b8: made consistent again.
made consistent again
Jun 22 2021, 4:04 PM

Jun 17 2021

florian.haftmann committed rAFP06eb6c7d6c76: lemma grooming.
lemma grooming
Jun 17 2021, 8:22 AM

Jun 16 2021

florian.haftmann committed rISABELLE52b829b18066: more lemmas.
more lemmas
Jun 16 2021, 10:33 AM
florian.haftmann committed rAFPc2595f7c289f: no duplicates of shift operations.
no duplicates of shift operations
Jun 16 2021, 10:23 AM

Jun 10 2021

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

Jun 6 2021

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

Jun 3 2021

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

Jun 2 2021

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

May 30 2021

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

May 29 2021

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

May 27 2021

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

May 17 2021

florian.haftmann committed rAFPe766628a0795: mere abbreviation for logical alias.
mere abbreviation for logical alias
May 17 2021, 12:33 PM
florian.haftmann committed rISABELLE4b1386b2c23e: mere abbreviation for logical alias.
mere abbreviation for logical alias
May 17 2021, 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