# User Details

User Details

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

# Sat, Oct 1

Sat, Oct 1

florian.haftmann committed rISABELLEa7ccb744047b: syntactic type classes for signed division operators.

syntactic type classes for signed division operators

reduce prominence of facts

# Thu, Sep 29

Thu, Sep 29

adjusted to distribution

florian.haftmann committed rISABELLE64e8d4afcf10: moved relevant theorems from theory Divides to theory Euclidean_Division.

moved relevant theorems from theory Divides to theory Euclidean_Division

# Mon, Sep 26

Mon, Sep 26

streamlined division on polynomials

# Sun, Sep 25

Sun, Sep 25

streamlined division on polynomials

adjusted to distribution

# Wed, Sep 21

Wed, Sep 21

streamlined division on polynomials

streamlined division on polynomials

# Wed, Sep 14

Wed, Sep 14

More on division concerning gauss numbers.

# Tue, Sep 13

Tue, Sep 13

florian.haftmann committed rISABELLEe7497a1de8b9: more concise instance-specific rules on euclidean relation.

more concise instance-specific rules on euclidean relation

# Mon, Sep 12

Mon, Sep 12

putting together related theorems

dropped auxiliary lemma

# Sat, Sep 10

Sat, Sep 10

less specialized euclidean relation on int

# Mon, Sep 5

Mon, Sep 5

clarified generic euclidean relation

# Aug 24 2022

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

avoid fact name clash

avoid looping simplification for z2

adjusted to distribution

# Aug 21 2022

Aug 21 2022

simplified computation algorithm construction

# Aug 20 2022

Aug 20 2022

tuned type signature

tuned type signature

streamlined theorems

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

consolidated attribute name

florian.haftmann committed rISABELLE24b17460ee60: streamlined simpset building, avoiding duplicated rewrite rules.

streamlined simpset building, avoiding duplicated rewrite rules

streamlined theorems

streamlined theorems and sections

# Aug 19 2022

Aug 19 2022

florian.haftmann committed rISABELLE48d032035744: streamlined primitive definitions for integer division.

streamlined primitive definitions for integer division

florian.haftmann committed rAFP3d7eaa9f630e: streamlined primitive definitions for integer division.

streamlined primitive definitions for integer division

# Aug 10 2022

Aug 10 2022

florian.haftmann committed rISABELLEa21debbc7074: Further streamlining of quick-and-dirty evaluation..

Further streamlining of quick-and-dirty evaluation.

Further streamlining of quick-and-dirty evaluation.

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.

# Jul 28 2022

Jul 28 2022

Some more proofs.

# Jul 25 2022

Jul 25 2022

Avoid shadowing original List._ namespace.

# Jul 12 2022

Jul 12 2022

refined code equations for characters

# Jul 10 2022

Jul 10 2022

refined code equations for characters

# Jul 6 2022

Jul 6 2022

removed more material now residing in distribution

florian.haftmann committed rAFP01df7496c94e: separated non-computable instance of bit comprehension from computable one.

separated non-computable instance of bit comprehension from computable one

sketch for word-specific lsb and msb

# Jul 5 2022

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…

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 4 2022

Jul 4 2022

corrections and adjustions for Scala 3

more complete set of code equations

florian.haftmann committed rISABELLE34cd1d210b92: officical abstract characters for code generation.

officical abstract characters for code generation

# Jun 26 2022

Jun 26 2022

florian.haftmann committed rISABELLE53b61706749b: Centralized some char-related lemmas in distribution..

Centralized some char-related lemmas in distribution.

# Jun 23 2022

Jun 23 2022

Avoid calculations where not necessary.

Avoid calculations where not necessary.

Prefer existing horner sum combinator.

Executable lexords.

# Jun 20 2022

Jun 20 2022

Avoid explicit operation when not necessary.

# Jun 16 2022

Jun 16 2022

Trimmed down dependencies.

# May 22 2022

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

# Apr 9 2022

Apr 9 2022

florian.haftmann committed rISABELLEe0fa345f1aab: documentation on diagnostic devices for code generation.

documentation on diagnostic devices for code generation

more correct language

# Apr 7 2022

Apr 7 2022

moved from AFP to distribution

moved from AFP to distribution

# Apr 3 2022

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

florian.haftmann committed rISABELLEcdf84288d93c: pass constructor arity as part of case certficiate.

pass constructor arity as part of case certficiate

tuned whitespace in generated code

# Apr 2 2022

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…

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 1 2022

Apr 1 2022

# Mar 29 2022

Mar 29 2022

NEWS and CONTRIBUTORS

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 28 2022

Mar 28 2022

separated treatment of undefined bodys

modernized handling of variables

tuned arguments

structurally tuned

prefer build combinator

tuned whitespace

# Mar 24 2022

Mar 24 2022

separated case reduction

separated selector function entirely

self-contained extraction auf clauses

florian.haftmann committed rISABELLEb7a74a04ae4e: extracted selector function, restoring code generation for let expressions.

extracted selector function, restoring code generation for let expressions

# Feb 24 2022

Feb 24 2022

simp rules for negative numerals

Clarified code module names.

removed ancient numeral representation