# User Details

User Details

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

# Fri, Jan 27

Fri, Jan 27

dropped reference to dead clone

removed dead clone

Tuned whitespace.

More correct references.

Updated references.

Restored antiquotation.

tuned whitespace

# Tue, Jan 24

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…

florian.haftmann committed rAFPdb93f67adfd0: generalized theory name: euclidean division denotes one particular division….

generalized theory name: euclidean division denotes one particular division…

more efficient specification

# Dec 17 2022

Dec 17 2022

prefer SML here

# Oct 28 2022

Oct 28 2022

modulus for polynomials is invariant wrt. units

# Oct 6 2022

Oct 6 2022

euclidean division on gaussian numbers

# Oct 4 2022

Oct 4 2022

slightly less abusive proof pattern

note on signed division on words

tuned definition

slightly less abusive proof pattern

# Oct 1 2022

Oct 1 2022

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

syntactic type classes for signed division operators

reduce prominence of facts

# Sep 29 2022

Sep 29 2022

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

# Sep 26 2022

Sep 26 2022

streamlined division on polynomials

# Sep 25 2022

Sep 25 2022

streamlined division on polynomials

adjusted to distribution

# Sep 21 2022

Sep 21 2022

streamlined division on polynomials

streamlined division on polynomials

# Sep 14 2022

Sep 14 2022

More on division concerning gauss numbers.

# Sep 13 2022

Sep 13 2022

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

more concise instance-specific rules on euclidean relation

# Sep 12 2022

Sep 12 2022

putting together related theorems

dropped auxiliary lemma

# Sep 10 2022

Sep 10 2022

less specialized euclidean relation on int

# Sep 5 2022

Sep 5 2022

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