Page MenuHomeIsabelle/Phabricator

florian.haftmann (Florian Haftmann)
User

Projects

User Details

User Since
Nov 30 2019, 9:26 AM (134 w, 4 d)

Recent Activity

Sun, Jun 26

florian.haftmann committed rISABELLE7a6301d01199: More lemmas..
More lemmas.
Sun, Jun 26, 5:24 PM
florian.haftmann committed rISABELLE53b61706749b: Centralized some char-related lemmas in distribution..
Centralized some char-related lemmas in distribution.
Sun, Jun 26, 5:24 PM

Thu, Jun 23

florian.haftmann committed rAFP46986ae57fb9: Avoid calculations where not necessary..
Avoid calculations where not necessary.
Thu, Jun 23, 9:25 AM
florian.haftmann committed rISABELLE5ec227251b07: Avoid calculations where not necessary..
Avoid calculations where not necessary.
Thu, Jun 23, 9:24 AM
florian.haftmann committed rISABELLE6de655ccac19: Prefer existing horner sum combinator..
Prefer existing horner sum combinator.
Thu, Jun 23, 9:24 AM
florian.haftmann committed rISABELLEd078f8482155: Less warnings..
Less warnings.
Thu, Jun 23, 9:24 AM
florian.haftmann committed rISABELLE36965f6b3530: Executable lexords..
Executable lexords.
Thu, Jun 23, 9:24 AM

Mon, Jun 20

florian.haftmann committed rAFP95b886c17e9a: Avoid explicit operation when not necessary..
Avoid explicit operation when not necessary.
Mon, Jun 20, 2:21 PM

Thu, Jun 16

florian.haftmann committed rAFP4eebdc219200: Trimmed down dependencies..
Trimmed down dependencies.
Thu, Jun 16, 1:26 PM

May 22 2022

florian.haftmann committed rISABELLE160c9c18a707: »nil« seems to be a reserved constructor word in PolyML.
»nil« seems to be a reserved constructor word in PolyML
May 22 2022, 8:02 AM

Apr 9 2022

florian.haftmann committed rISABELLEe0fa345f1aab: documentation on diagnostic devices for code generation.
documentation on diagnostic devices for code generation
Apr 9 2022, 11:41 AM
florian.haftmann committed rISABELLE7b75a2c5b142: more correct language.
more correct language
Apr 9 2022, 11:28 AM

Apr 7 2022

florian.haftmann committed rAFP509270282029: moved from AFP to distribution.
moved from AFP to distribution
Apr 7 2022, 9:35 AM
florian.haftmann committed rAFPcb5230a8e3a2: tuned syntax.
tuned syntax
Apr 7 2022, 9:35 AM
florian.haftmann committed rISABELLE3f24cc294d74: moved from AFP to distribution.
moved from AFP to distribution
Apr 7 2022, 9:35 AM

Apr 3 2022

florian.haftmann committed rISABELLE010a77180dff: adjusted printing of type annotations to accomodate Scala 3.
adjusted printing of type annotations to accomodate Scala 3
Apr 3 2022, 4:21 PM
florian.haftmann committed rISABELLEcdf84288d93c: pass constructor arity as part of case certficiate.
pass constructor arity as part of case certficiate
Apr 3 2022, 11:09 AM
florian.haftmann committed rISABELLEa58718427bff: tuned whitespace in generated code.
tuned whitespace in generated code
Apr 3 2022, 11:09 AM

Apr 2 2022

florian.haftmann committed rAFP667d48034562: avoid side effects on working copy while runnign sessions (generated code is….
avoid side effects on working copy while runnign sessions (generated code is…
Apr 2 2022, 8:43 AM
florian.haftmann committed rISABELLEe852c776a455: tuned, centralizing case distinction at one place at the cost of modest….
tuned, centralizing case distinction at one place at the cost of modest…
Apr 2 2022, 8:27 AM

Apr 1 2022

florian.haftmann committed rISABELLE2c3eadf5ca6f: tuned.
tuned
Apr 1 2022, 6:36 PM
florian.haftmann committed rISABELLE047e1aaa0f06: tuned.
tuned
Apr 1 2022, 6:36 PM

Mar 29 2022

florian.haftmann committed rISABELLE366f85a10407: NEWS and CONTRIBUTORS.
NEWS and CONTRIBUTORS
Mar 29 2022, 3:45 PM
florian.haftmann committed rISABELLE4b8da5eef9d0: regenerated.
regenerated
Mar 29 2022, 8:07 AM
florian.haftmann committed rISABELLEf9c758208298: tighter check to ensure that patterns remain left-linear, previous….
tighter check to ensure that patterns remain left-linear, previous…
Mar 29 2022, 8:07 AM
florian.haftmann committed rISABELLE528768bc7bd0: tuned.
tuned
Mar 29 2022, 8:07 AM
florian.haftmann committed rISABELLE1d08a01a7abb: tuned.
tuned
Mar 29 2022, 8:07 AM

Mar 28 2022

florian.haftmann committed rISABELLE75c69cbffe5f: separated treatment of undefined bodys.
separated treatment of undefined bodys
Mar 28 2022, 10:04 PM
florian.haftmann committed rISABELLEfa014f31f208: modernized handling of variables.
modernized handling of variables
Mar 28 2022, 10:04 PM
florian.haftmann committed rISABELLE9257e7732766: tuned arguments.
tuned arguments
Mar 28 2022, 10:04 PM
florian.haftmann committed rISABELLE26206ade1a23: structurally tuned.
structurally tuned
Mar 28 2022, 8:24 AM
florian.haftmann committed rISABELLEcbefaa400da2: tuned names.
tuned names
Mar 28 2022, 8:24 AM
florian.haftmann committed rISABELLE05f7f5454cb6: prefer build combinator.
prefer build combinator
Mar 28 2022, 8:24 AM
florian.haftmann committed rISABELLE96c19d03b5a5: tuned whitespace.
tuned whitespace
Mar 28 2022, 8:24 AM

Mar 24 2022

florian.haftmann committed rISABELLE89d975dd39f1: tuned.
tuned
Mar 24 2022, 10:21 PM
florian.haftmann committed rISABELLE96da582011ae: separated case reduction.
separated case reduction
Mar 24 2022, 10:21 PM
florian.haftmann committed rISABELLE21897aad78ad: separated selector function entirely.
separated selector function entirely
Mar 24 2022, 10:21 PM
florian.haftmann committed rISABELLEa82f7f8a3c7b: self-contained extraction auf clauses.
self-contained extraction auf clauses
Mar 24 2022, 10:21 PM
florian.haftmann committed rISABELLEd06547c72775: streamlined.
streamlined
Mar 24 2022, 10:21 PM
florian.haftmann committed rISABELLEb7a74a04ae4e: extracted selector function, restoring code generation for let expressions.
extracted selector function, restoring code generation for let expressions
Mar 24 2022, 10:21 PM
florian.haftmann committed rISABELLEfd3d66066256: streamlined.
streamlined
Mar 24 2022, 10:21 PM
florian.haftmann committed rISABELLEa2c5efb7298a: disentangled.
disentangled
Mar 24 2022, 10:21 PM
florian.haftmann committed rISABELLEc7ff16398535: streamlined.
streamlined
Mar 24 2022, 10:21 PM

Feb 24 2022

florian.haftmann committed rISABELLEcd77ffb01e15: simp rules for negative numerals.
simp rules for negative numerals
Feb 24 2022, 5:19 PM
florian.haftmann committed rAFPf9f890f6481e: Clarified code module names..
Clarified code module names.
Feb 24 2022, 5:18 PM
florian.haftmann committed rAFP053a95296353: removed ancient numeral representation.
removed ancient numeral representation
Feb 24 2022, 5:18 PM

Feb 18 2022

florian.haftmann committed rAFP29febbf375f9: Another attempt for a consolidated terminology..
Another attempt for a consolidated terminology.
Feb 18 2022, 1:08 PM

Feb 17 2022

florian.haftmann committed rAFPb79723149239: Avoid overaggresive splitting..
Avoid overaggresive splitting.
Feb 17 2022, 9:39 PM
florian.haftmann committed rAFPa64cb91acc6c: more lemmas for distribution.
more lemmas for distribution
Feb 17 2022, 9:39 PM
florian.haftmann committed rAFP9aef984d878b: Avoid overaggresive simplification..
Avoid overaggresive simplification.
Feb 17 2022, 9:39 PM
florian.haftmann committed rISABELLEf3fcc7c5a0db: Avoid overaggresive splitting..
Avoid overaggresive splitting.
Feb 17 2022, 9:37 PM
florian.haftmann committed rISABELLEccc3a72210e6: Avoid overaggresive simplification..
Avoid overaggresive simplification.
Feb 17 2022, 9:37 PM
florian.haftmann committed rISABELLE4cc719621825: more lemmas for distribution.
more lemmas for distribution
Feb 17 2022, 9:37 PM

Feb 12 2022

florian.haftmann committed rISABELLE78c2a92a8be4: updated documentation to current matter of affairs.
updated documentation to current matter of affairs
Feb 12 2022, 7:56 AM

Jan 11 2022

florian.haftmann committed rISABELLE1f30aa91f496: more correct transfer.
more correct transfer
Jan 11 2022, 8:02 PM
florian.haftmann committed rISABELLE4d77dd3019d1: earlier availability of lifting.
earlier availability of lifting
Jan 11 2022, 8:02 PM
florian.haftmann committed rAFPd858bca8a11d: tuned.
tuned
Jan 11 2022, 8:01 PM

Nov 2 2021

florian.haftmann committed rAFPb40b44b920f5: restored theory structure for simple genericity..
restored theory structure for simple genericity.
Nov 2 2021, 1:46 PM
florian.haftmann added a reverting change for rAFPaf549be0a8cd: restored different entrance points a before Isabelle2021: rAFP7825cfb5f214: Backed out changeset af549be0a8cd.
Nov 2 2021, 8:28 AM
florian.haftmann committed rAFP7825cfb5f214: Backed out changeset af549be0a8cd.
Backed out changeset af549be0a8cd
Nov 2 2021, 8:28 AM
florian.haftmann committed rAFPaf549be0a8cd: restored different entrance points a before Isabelle2021.
restored different entrance points a before Isabelle2021
Nov 2 2021, 8:25 AM

Nov 1 2021

florian.haftmann committed rAFPef2487130488: Adjusted to prospective release Isabelle2021-2..
Adjusted to prospective release Isabelle2021-2.
Nov 1 2021, 11:02 AM

Oct 29 2021

florian.haftmann committed rISABELLE43142ac556e6: moved generic implementation into HOL-Main.
moved generic implementation into HOL-Main
Oct 29 2021, 10:34 AM

Oct 26 2021

florian.haftmann committed rAFP99b814982902: more generic bit/word lemmas for distribution.
more generic bit/word lemmas for distribution
Oct 26 2021, 5:23 PM
florian.haftmann committed rISABELLE3c587b7c3d5c: more generic bit/word lemmas for distribution.
more generic bit/word lemmas for distribution
Oct 26 2021, 5:23 PM

Oct 24 2021

florian.haftmann committed rAFPb7f45664e583: back to dedicated separate shift operations for infix syntax;.
back to dedicated separate shift operations for infix syntax;
Oct 24 2021, 8:09 AM

Oct 14 2021

florian.haftmann committed rAFPb29e73d246d4: bit singleton shifts recovered for the sake of backward compatibility.
bit singleton shifts recovered for the sake of backward compatibility
Oct 14 2021, 9:54 AM

Oct 11 2021

florian.haftmann committed rAFP134b70fc858e: primer.
primer
Oct 11 2021, 9:41 PM
florian.haftmann committed rISABELLE27475e64a887: more complete simp rules.
more complete simp rules
Oct 11 2021, 1:26 PM
florian.haftmann committed rAFPf8dc7663c3cf: more complete simp rules.
more complete simp rules
Oct 11 2021, 1:25 PM
florian.haftmann committed rAFP052886ce16c0: more complete simp rules (examples).
more complete simp rules (examples)
Oct 11 2021, 8:33 AM
florian.haftmann committed rISABELLE9c04a82c3128: more complete simp rules.
more complete simp rules
Oct 11 2021, 8:32 AM

Oct 10 2021

florian.haftmann committed rISABELLE807b094a9b78: avoid overaggressive contraction of conversions.
avoid overaggressive contraction of conversions
Oct 10 2021, 5:46 PM
florian.haftmann committed rAFPc42c2c2447c2: avoid overaggressive contraction of conversions.
avoid overaggressive contraction of conversions
Oct 10 2021, 5:45 PM
florian.haftmann committed rAFP721d0f625e02: slightly more prominence for proof tools; more examples.
slightly more prominence for proof tools; more examples
Oct 10 2021, 8:02 AM
florian.haftmann committed rISABELLEbc27c490aaac: normalizing NOT (numeral _) (again).
normalizing NOT (numeral _) (again)
Oct 10 2021, 8:01 AM

Sep 29 2021

florian.haftmann committed rAFP1ab5075701b4: repaired slip.
repaired slip
Sep 29 2021, 10:59 AM
florian.haftmann committed rISABELLE930047942f46: repaired slip.
repaired slip
Sep 29 2021, 10:57 AM

Sep 26 2021

florian.haftmann committed rISABELLE99add5178e51: NOT is part of syntax bundle also.
NOT is part of syntax bundle also
Sep 26 2021, 11:25 AM

Sep 24 2021

florian.haftmann committed rISABELLE690928dd6f8f: apply declarations from interpretations in eigen context also.
apply declarations from interpretations in eigen context also
Sep 24 2021, 7:32 PM

Sep 13 2021

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…
Sep 13 2021, 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…
Sep 13 2021, 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