User Details
User Details
- User Since
- Nov 19 2019, 1:16 PM (200 w, 3 d)
Jun 2 2023
Jun 2 2023
fixed some ACM/AMS categories
fixed broken LaTeX quotation marks in abstracts
recategorised some entries
sitegen for Schwartz_Zippel
new topic: Computer science/Algorithms/Randomized
new entry: Schwartz_Zippel
Jan 24 2023
Jan 24 2023
fixed broken abstract for PAPP_Impossibility
Sep 23 2022
Sep 23 2022
sitegen for Padic_Field
sitegen for Risk_Free_Lending
pruvisto committed rAFP802687e3f62a: new entry: Padic_Field.
new entry: Padic_Field
new entry: Risk_Free_Lending
Sep 8 2022
Sep 8 2022
sitegen for Number_Theoretic_Transform
fixed metadata for Hales_Jewett
new entry Number_Theoretic_Transform
Aug 23 2022
Aug 23 2022
sitegen for Commuting_Hermitian
new entry: Commuting_Hermitian
Jul 20 2022
Jul 20 2022
XZ compression for Safe_Distance examples (safes 160 MB!)
Jul 18 2022
Jul 18 2022
pruvisto committed rAFP74eeeedd2e19: ORCID for Manuel Eberl.
ORCID for Manuel Eberl
name change for Kądziołka
name change for Kądziołka
May 10 2022
May 10 2022
updated name and email address of Rose Bohrer
May 9 2022
May 9 2022
updated name and email address of Rose Bohrer
Nov 16 2021
Nov 16 2021
more material for HOL-Analysis.Infinite_Sum
adapted to new version of Infinite_Sum in isabelle-dev
Nov 14 2021
Nov 14 2021
changed affiliation of eberl (this time properly)
changed affiliation of Eberl
Nov 9 2021
Nov 9 2021
changed affiliation of eberl (this time properly)
changed affiliation of eberl
Oct 19 2021
Oct 19 2021
updated website/email address
pruvisto committed rISABELLEd592354c4a26: removed some 'private' modifiers from HOL-Computational_Algebra.
removed some 'private' modifiers from HOL-Computational_Algebra
updated email address
Oct 7 2021
Oct 7 2021
adapted QHLProver to isabelle-dev/409ca22dee4c
adapted to isabelle-dev/409ca22dee4c
pruvisto committed rISABELLE409ca22dee4c: new notion of infinite sums in HOL-Analysis, ordering on complex numbers.
new notion of infinite sums in HOL-Analysis, ordering on complex numbers
Jul 26 2021
Jul 26 2021
Added Finitely_Generated_Abelian_Groups to metadata
Jul 7 2021
Jul 7 2021
Added missing Public_Announcement_Logic to ROOTS file
May 27 2021
May 27 2021
pruvisto committed rAFPcddbe565783d: sitegen for Padic_Ints.
sitegen for Padic_Ints
pruvisto committed rAFPf463e6d25245: new entry: Padic_Ints.
new entry: Padic_Ints
Apr 7 2021
Apr 7 2021
pruvisto committed rISABELLE56db8559eadb: fixed problematic addition operation in the 'approximation' package (previous….
fixed problematic addition operation in the 'approximation' package (previous…
adapted to isabelle-dev/56db8559eadb
Mar 3 2021
Mar 3 2021
Tuned presentation of Buffon's needle
Feb 19 2021
Feb 19 2021
pruvisto committed rISABELLEf6bb31879698: HOL-Analysis/Probability: Hoeffding's inequality, negative binomial….
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial…
adapted to isabelle-dev/73253:f6bb31879698
Feb 18 2021
Feb 18 2021
Buffons_Needle: tuned presentation
pruvisto committed rAFPbcfe34497000: Ergodic_Theory: removed 'pullback_algebra'. Turns out it already exists and is….
Ergodic_Theory: removed 'pullback_algebra'. Turns out it already exists and is…
Feb 11 2021
Feb 11 2021
Ergodic_Theory: tuned some names
Ergodic_Theory: ergodicity of the shift operator
Feb 10 2021
Feb 10 2021
Ergodic_Theory: tuned some names
Ergodic_Theory: ergodicity of the shift operator
Feb 2 2021
Feb 2 2021
fixed category for Blue_Eyes
pruvisto added a reverting change for rAFP4450302adc70: fixed category for Blue_Eyes: rAFP357a81dcd962: Backed out changeset 4450302adc70.
Backed out changeset 4450302adc70
fixed category for Blue_Eyes
pruvisto committed rAFPd5d57c1027c0: sitegen for Blue_Eyes.
sitegen for Blue_Eyes
Jan 13 2021
Jan 13 2021
pruvisto committed rAFPdd8e0cdca49e: sitegen for CSP_RefTK.
sitegen for CSP_RefTK
New submission: CSP_RefTK
Jan 9 2021
Jan 9 2021
pruvisto committed rISABELLE9bf36baa8686: Corrected lemma that was too specific in HOL-Computational_Algebra.
Corrected lemma that was too specific in HOL-Computational_Algebra
Jan 8 2021
Jan 8 2021
Algebraic_Numbers: some material on algebraic integers
pruvisto committed rISABELLE783406dd051e: some algebra material for HOL: characteristic of a ring, algebraic integers.
some algebra material for HOL: characteristic of a ring, algebraic integers
pruvisto committed rISABELLE981a383610df: HOL-Data_Structures: added Selection and time functions for list functions.
HOL-Data_Structures: added Selection and time functions for list functions
Jan 5 2021
Jan 5 2021
pruvisto committed rISABELLEc03a148110cc: HOL-Library.Multiset: new notation for prod_mset, consistent with sum_mset.
HOL-Library.Multiset: new notation for prod_mset, consistent with sum_mset
pruvisto committed rAFP8bf81decb8ac: adapted to isabelle-dev/74be162a47cd: added some renamings that were missed….
adapted to isabelle-dev/74be162a47cd: added some renamings that were missed…
Jan 4 2021
Jan 4 2021
adapted to isabelle-dev/74be162a47cd
pruvisto committed rISABELLE7ad9f197ca7e: HOL-Complex_Analysis: coefficient asymptotics for meromorphic functions.
HOL-Complex_Analysis: coefficient asymptotics for meromorphic functions
HOL-Library: Changed notation for sum_mset
Sep 8 2020
Sep 8 2020
sitegen for PAC_Checker
Aug 26 2020
Aug 26 2020
sitegen for Ordinal_Partitions
New entry: Ordinal_Partitions
sitegen for Amicable_Numbers
New entry: Amicable_Numbers
Jun 26 2020
Jun 26 2020
added missing HTML file
new entry Nash_Williams
sitegen for Nash_Williams
May 17 2020
May 17 2020
sitegen for Matrices_for_ODEs
New entry: Matrices_for_ODEs
New entry LTL_Normal_Form
sitegen for LTL_Normal_Form
Fixed missing MathJax fonts
May 15 2020
May 15 2020
adapted to isabelle-dev/07c85c68ff03
pruvisto committed rISABELLE07c85c68ff03: added missing preprocessing step for extraction (due to Stefan Berghofer).
added missing preprocessing step for extraction (due to Stefan Berghofer)
new HOL simproc: eliminate_false_implies
May 14 2020
May 14 2020
Tuned some proofs in HOL-Analysis
May 13 2020
May 13 2020
generalised pigeonhole principle in HOL-Library.FuncSet
new constant power_int in HOL
New HOL simproc 'datatype_no_proper_subterm'
adapted to isabelle-dev/c095d3143047
May 4 2020
May 4 2020
Backed out changeset c78f358a496d
pruvisto added a reverting change for rAFPc78f358a496d: Adapted to isabelle-dev/159e33bdddc6: rAFPdfe61dcb44e3: Backed out changeset c78f358a496d.
More robust proof in Slicing
Adapted to isabelle-dev/159e33bdddc6
More robust apply proofs in Finger-Trees
Extended Stirling's formula to complex numbers
Apr 29 2020
Apr 29 2020
pruvisto committed rAFP1bfe40641dd3: Another attempt to fix MathJax + Jenkins: more robust ROOT_PATH in templates.
Another attempt to fix MathJax + Jenkins: more robust ROOT_PATH in templates
Tuned MathJax templates
Added MathJax support for abstracts
Documentation for MathJax
Another attempt to fix MathJax on Jenkins 2
Another attempt to fix MathJax on Jenkins