User Details
User Details
- User Since
- Nov 30 2019, 9:26 AM (198 w, 6 d)
Sat, Sep 16
Sat, Sep 16
reduced prominence of lemma names
reduced prominence of lemma names
new formulation of an auxiliary lemma
Thu, Sep 14
Thu, Sep 14
Corrected type calculation.
some hints on managed installations
florian.haftmann committed rISABELLEd052d61da398: prefer cartouches over quotes for clarity of resulting document.
prefer cartouches over quotes for clarity of resulting document
May 3 2023
May 3 2023
stripped unused functionality
May 2 2023
May 2 2023
florian.haftmann committed rISABELLEb41c8fce442d: case translation in intermediate language eliminates semantic clone.
case translation in intermediate language eliminates semantic clone
Apr 30 2023
Apr 30 2023
more correct type calculation
Backed out changeset 5016262a2384
Apr 20 2023
Apr 20 2023
clarified terminology
Apr 11 2023
Apr 11 2023
some remarks on division
no subsection without section
clarified scope of document
some remarks on division
proper section headings
Mar 24 2023
Mar 24 2023
Adjusted to changes in distribution.
florian.haftmann committed rISABELLEa6a81f848135: More explicit type information in dictionary arguments..
More explicit type information in dictionary arguments.
tuned whitespace
florian.haftmann committed rISABELLE4c5297aa18c8: more uniform approach towards satisfied applications.
more uniform approach towards satisfied applications
florian.haftmann committed rISABELLE0262155d2743: more uniform approach towards satisfied applications.
more uniform approach towards satisfied applications
Tuned semicolons.
Feb 12 2023
Feb 12 2023
somehow more clear terminology
somehow more clear terminology
Feb 9 2023
Feb 9 2023
actually executable enum_all, enum_ex for word
Jan 27 2023
Jan 27 2023
dropped reference to dead clone
removed dead clone
Tuned whitespace.
More correct references.
Updated references.
Restored antiquotation.
tuned whitespace
Jan 24 2023
Jan 24 2023
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.