Page MenuHomeIsabelle/Phabricator

florian.haftmann (Florian Haftmann)
User

Projects

User Details

User Since
Nov 30 2019, 9:26 AM (148 w, 2 d)

Recent Activity

Sat, Oct 1

florian.haftmann committed rISABELLEa7ccb744047b: syntactic type classes for signed division operators.
syntactic type classes for signed division operators
Sat, Oct 1, 5:53 PM
florian.haftmann committed rAFPa74db29363f5: tuned proofs.
tuned proofs
Sat, Oct 1, 3:08 PM
florian.haftmann committed rISABELLE8a48e18f081e: reduce prominence of facts.
reduce prominence of facts
Sat, Oct 1, 3:08 PM

Thu, Sep 29

florian.haftmann committed rAFP474696083e43: adjusted to distribution.
adjusted to distribution
Thu, Sep 29, 4:17 PM
florian.haftmann committed rISABELLE64e8d4afcf10: moved relevant theorems from theory Divides to theory Euclidean_Division.
moved relevant theorems from theory Divides to theory Euclidean_Division
Thu, Sep 29, 4:16 PM

Mon, Sep 26

florian.haftmann committed rISABELLE14dd8b46307f: streamlined division on polynomials.
streamlined division on polynomials
Mon, Sep 26, 12:30 PM

Sun, Sep 25

florian.haftmann committed rISABELLE8fcbce9f317c: streamlined division on polynomials.
streamlined division on polynomials
Sun, Sep 25, 9:26 PM
florian.haftmann committed rAFP5e7974c944c6: adjusted to distribution.
adjusted to distribution
Sun, Sep 25, 9:16 PM

Wed, Sep 21

florian.haftmann committed rISABELLEd435f7b57212: streamlined division on polynomials.
streamlined division on polynomials
Wed, Sep 21, 7:41 AM
florian.haftmann committed rAFPbccf6f281b7b: streamlined division on polynomials.
streamlined division on polynomials
Wed, Sep 21, 7:36 AM

Wed, Sep 14

florian.haftmann committed rISABELLEe278bf6430cf: More on division concerning gauss numbers..
More on division concerning gauss numbers.
Wed, Sep 14, 1:05 PM

Tue, Sep 13

florian.haftmann committed rISABELLEe7497a1de8b9: more concise instance-specific rules on euclidean relation.
more concise instance-specific rules on euclidean relation
Tue, Sep 13, 8:00 PM

Mon, Sep 12

florian.haftmann committed rISABELLEf58ad163bb75: putting together related theorems.
putting together related theorems
Mon, Sep 12, 1:31 PM
florian.haftmann committed rISABELLE3ae579092045: dropped auxiliary lemma.
dropped auxiliary lemma
Mon, Sep 12, 10:07 AM

Sat, Sep 10

florian.haftmann committed rAFP34a31d29f666: streamlined.
streamlined
Sat, Sep 10, 4:07 PM
florian.haftmann committed rISABELLE98cab94326d4: less specialized euclidean relation on int.
less specialized euclidean relation on int
Sat, Sep 10, 4:06 PM

Mon, Sep 5

florian.haftmann committed rISABELLE3310317cc484: clarified generic euclidean relation.
clarified generic euclidean relation
Mon, Sep 5, 4:49 PM

Aug 24 2022

florian.haftmann committed rISABELLE884dbbc8e1b3: avoid duplicate fact error on global_interpretation of residues.
avoid duplicate fact error on global_interpretation of residues
Aug 24 2022, 10:26 AM
florian.haftmann committed rAFPf50360e11df7: avoid fact name clash.
avoid fact name clash
Aug 24 2022, 10:26 AM
florian.haftmann committed rISABELLEc530cb79ccbc: avoid looping simplification for z2.
avoid looping simplification for z2
Aug 24 2022, 8:46 AM
florian.haftmann committed rAFPcf809a286330: adjusted to distribution.
adjusted to distribution
Aug 24 2022, 8:44 AM
florian.haftmann committed rAFP939afa7484fc: repaired proof.
repaired proof
Aug 24 2022, 8:21 AM

Aug 21 2022

florian.haftmann committed rISABELLE5305c65dcbb2: Gauss numbers.
Gauss numbers
Aug 21 2022, 11:26 PM
florian.haftmann committed rISABELLE02b18f59f903: streamlined.
streamlined
Aug 21 2022, 8:43 AM
florian.haftmann committed rISABELLEd2e6a1342c90: simplified computation algorithm construction.
simplified computation algorithm construction
Aug 21 2022, 8:43 AM
florian.haftmann committed rAFP59b0a80cf40b: streamlined.
streamlined
Aug 21 2022, 8:43 AM

Aug 20 2022

florian.haftmann committed rISABELLE96d5fa32f0f7: tuned type signature.
tuned type signature
Aug 20 2022, 8:59 AM
florian.haftmann committed rISABELLEd7e0b6620c07: tuned type signature.
tuned type signature
Aug 20 2022, 8:59 AM
florian.haftmann committed rISABELLE83e4b6a5e7de: streamlined theorems.
streamlined theorems
Aug 20 2022, 8:59 AM
florian.haftmann committed rISABELLE714fad33252e: more thorough split rules for div and mod on numerals, tuned split rules setup.
more thorough split rules for div and mod on numerals, tuned split rules setup
Aug 20 2022, 8:59 AM
florian.haftmann committed rISABELLEfcd118d9242f: consolidated attribute name.
consolidated attribute name
Aug 20 2022, 8:59 AM
florian.haftmann committed rISABELLE24b17460ee60: streamlined simpset building, avoiding duplicated rewrite rules.
streamlined simpset building, avoiding duplicated rewrite rules
Aug 20 2022, 8:59 AM
florian.haftmann committed rISABELLEdc758531077b: streamlined theorems.
streamlined theorems
Aug 20 2022, 8:59 AM
florian.haftmann committed rISABELLE647879691c1c: streamlined theorems and sections.
streamlined theorems and sections
Aug 20 2022, 8:59 AM
florian.haftmann committed rAFP26a20c98b97c: tuned proofs.
tuned proofs
Aug 20 2022, 8:57 AM

Aug 19 2022

florian.haftmann committed rISABELLE48d032035744: streamlined primitive definitions for integer division.
streamlined primitive definitions for integer division
Aug 19 2022, 7:49 AM
florian.haftmann committed rAFP3d7eaa9f630e: streamlined primitive definitions for integer division.
streamlined primitive definitions for integer division
Aug 19 2022, 7:47 AM

Aug 10 2022

florian.haftmann committed rISABELLEa21debbc7074: Further streamlining of quick-and-dirty evaluation..
Further streamlining of quick-and-dirty evaluation.
Aug 10 2022, 10:33 PM
florian.haftmann committed rAFPeca5cf0e4817: Further streamlining of quick-and-dirty evaluation..
Further streamlining of quick-and-dirty evaluation.
Aug 10 2022, 10:29 PM
florian.haftmann committed rAFPcabf521b7579: An attempt for an integrated solution for quick-and-dirty evaluation..
An attempt for an integrated solution for quick-and-dirty evaluation.
Aug 10 2022, 4:52 PM

Jul 28 2022

florian.haftmann committed rISABELLE40af1efeadee: More lemmas..
More lemmas.
Jul 28 2022, 7:15 PM
florian.haftmann committed rISABELLEff0aceed8923: Some more proofs..
Some more proofs.
Jul 28 2022, 4:50 PM

Jul 25 2022

florian.haftmann committed rISABELLE1b812435a632: Avoid shadowing original List._ namespace..
Avoid shadowing original List._ namespace.
Jul 25 2022, 9:25 PM

Jul 12 2022

florian.haftmann committed rISABELLE714528f42922: refined code equations for characters.
refined code equations for characters
Jul 12 2022, 3:25 PM

Jul 10 2022

florian.haftmann committed rISABELLEed15f2cd4f7d: refined code equations for characters.
refined code equations for characters
Jul 10 2022, 9:08 PM

Jul 6 2022

florian.haftmann committed rAFPe68b946939fa: tuned.
tuned
Jul 6 2022, 10:02 PM
florian.haftmann committed rAFP521e4864b960: removed more material now residing in distribution.
removed more material now residing in distribution
Jul 6 2022, 10:02 PM
florian.haftmann committed rAFP01df7496c94e: separated non-computable instance of bit comprehension from computable one.
separated non-computable instance of bit comprehension from computable one
Jul 6 2022, 10:02 PM
florian.haftmann committed rISABELLEbe0865060346: sketch for word-specific lsb and msb.
sketch for word-specific lsb and msb
Jul 6 2022, 10:02 PM

Jul 5 2022

florian.haftmann committed rISABELLEf4116b7a6679: Move code lemmas for symbolic computation of bit operations on int to….
Move code lemmas for symbolic computation of bit operations on int to…
Jul 5 2022, 4:41 PM
florian.haftmann committed rAFPb48c96946723: Move code lemmas for symbolic computation of bit operations on int to….
Move code lemmas for symbolic computation of bit operations on int to…
Jul 5 2022, 4:41 PM

Jul 4 2022

florian.haftmann committed rISABELLE7afb6628ab86: corrections and adjustions for Scala 3.
corrections and adjustions for Scala 3
Jul 4 2022, 6:12 PM
florian.haftmann committed rISABELLEaa0403e5535f: more complete set of code equations.
more complete set of code equations
Jul 4 2022, 12:06 PM
florian.haftmann committed rISABELLE34cd1d210b92: officical abstract characters for code generation.
officical abstract characters for code generation
Jul 4 2022, 12:06 PM

Jun 26 2022

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

Jun 23 2022

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

Jun 20 2022

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

Jun 16 2022

florian.haftmann committed rAFP4eebdc219200: Trimmed down dependencies..
Trimmed down dependencies.
Jun 16 2022, 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