Page MenuHomeIsabelle/Phabricator

florian.haftmann (Florian Haftmann)
User

Projects

User Details

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

Recent Activity

Fri, Jan 27

florian.haftmann committed rAFP45600ccea74a: dropped reference to dead clone.
dropped reference to dead clone
Fri, Jan 27, 7:18 PM
florian.haftmann committed rAFPbcc172c19476: modernized.
modernized
Fri, Jan 27, 7:18 PM
florian.haftmann committed rAFP7be2c9c3f37c: removed dead clone.
removed dead clone
Fri, Jan 27, 7:18 PM
florian.haftmann committed rAFP897e5e348bf9: Modernized..
Modernized.
Fri, Jan 27, 7:17 PM
florian.haftmann committed rAFPc5fcab8016bf: More instances..
More instances.
Fri, Jan 27, 7:17 PM
florian.haftmann committed rAFP970e2a3dcdf1: Tuned whitespace..
Tuned whitespace.
Fri, Jan 27, 7:17 PM
florian.haftmann committed rAFPce0774eaa992: More correct references..
More correct references.
Fri, Jan 27, 7:17 PM
florian.haftmann committed rAFP72313706f65d: Updated references..
Updated references.
Fri, Jan 27, 7:17 PM
florian.haftmann committed rISABELLE4c4d40913900: Restored antiquotation..
Restored antiquotation.
Fri, Jan 27, 7:17 PM
florian.haftmann committed rISABELLE5ef443fa4a5d: tuned whitespace.
tuned whitespace
Fri, Jan 27, 7:16 PM

Tue, Jan 24

florian.haftmann committed rISABELLE5de3772609ea: generalized theory name: euclidean division denotes one particular division….
generalized theory name: euclidean division denotes one particular division…
Tue, Jan 24, 12:00 PM
florian.haftmann committed rAFPdb93f67adfd0: generalized theory name: euclidean division denotes one particular division….
generalized theory name: euclidean division denotes one particular division…
Tue, Jan 24, 12:00 PM
florian.haftmann committed rAFP75e99d0e6664: more efficient specification.
more efficient specification
Tue, Jan 24, 12:00 PM

Dec 17 2022

florian.haftmann committed rISABELLE89f78f76df1c: prefer SML here.
prefer SML here
Dec 17 2022, 10:19 AM
florian.haftmann committed rISABELLE2afbd514b654: Typo..
Typo.
Dec 17 2022, 10:19 AM

Oct 28 2022

florian.haftmann committed rISABELLE8cb141384682: restructured.
restructured
Oct 28 2022, 3:30 PM
florian.haftmann committed rISABELLE6bc3bb9d0e3e: modulus for polynomials is invariant wrt. units.
modulus for polynomials is invariant wrt. units
Oct 28 2022, 3:30 PM

Oct 6 2022

florian.haftmann committed rISABELLEfbde7d1211fc: euclidean division on gaussian numbers.
euclidean division on gaussian numbers
Oct 6 2022, 6:36 PM
florian.haftmann committed rISABELLE63bcec915790: tuned proof.
tuned proof
Oct 6 2022, 6:36 PM

Oct 4 2022

florian.haftmann committed rAFPad6ac3e1e898: slightly less abusive proof pattern.
slightly less abusive proof pattern
Oct 4 2022, 5:50 PM
florian.haftmann committed rISABELLE4a064fad28b2: note on signed division on words.
note on signed division on words
Oct 4 2022, 5:49 PM
florian.haftmann committed rISABELLEda4e57d30579: tuned definition.
tuned definition
Oct 4 2022, 5:49 PM
florian.haftmann committed rISABELLEe19d4c1c48ce: spelling.
spelling
Oct 4 2022, 5:49 PM
florian.haftmann committed rISABELLEc9ea813f92f2: tuned proof.
tuned proof
Oct 4 2022, 5:49 PM
florian.haftmann committed rISABELLE4111c94657b4: slightly less abusive proof pattern.
slightly less abusive proof pattern
Oct 4 2022, 5:49 PM

Oct 1 2022

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

Sep 29 2022

florian.haftmann committed rAFP474696083e43: adjusted to distribution.
adjusted to distribution
Sep 29 2022, 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
Sep 29 2022, 4:16 PM

Sep 26 2022

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

Sep 25 2022

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

Sep 21 2022

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

Sep 14 2022

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

Sep 13 2022

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

Sep 12 2022

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

Sep 10 2022

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

Sep 5 2022

florian.haftmann committed rISABELLE3310317cc484: clarified generic euclidean relation.
clarified generic euclidean relation
Sep 5 2022, 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