Page MenuHomeIsabelle/Phabricator

pruvisto (Manuel Eberl)
User

Projects

User Details

User Since
Nov 19 2019, 1:16 PM (157 w, 5 d)

Recent Activity

Sep 23 2022

pruvisto committed rAFP58d7766b8964: sitegen for Padic_Field.
sitegen for Padic_Field
Sep 23 2022, 5:57 PM
pruvisto committed rAFPb4ba256202a1: sitegen for Risk_Free_Lending.
sitegen for Risk_Free_Lending
Sep 23 2022, 5:57 PM
pruvisto committed rAFP802687e3f62a: new entry: Padic_Field.
new entry: Padic_Field
Sep 23 2022, 5:57 PM
pruvisto committed rAFP7bce0418a16a: new entry: Risk_Free_Lending.
new entry: Risk_Free_Lending
Sep 23 2022, 5:57 PM

Sep 8 2022

pruvisto committed rAFP7a3ce4a5cdf8: sitegen for Number_Theoretic_Transform.
sitegen for Number_Theoretic_Transform
Sep 8 2022, 7:10 PM
pruvisto committed rAFP4b1af6f3fd24: fixed metadata for Hales_Jewett.
fixed metadata for Hales_Jewett
Sep 8 2022, 7:10 PM
pruvisto committed rAFP9480bd426471: new entry Number_Theoretic_Transform.
new entry Number_Theoretic_Transform
Sep 8 2022, 7:10 PM

Aug 23 2022

pruvisto committed rAFPd7c911450d76: sitegen for Commuting_Hermitian.
sitegen for Commuting_Hermitian
Aug 23 2022, 9:32 AM
pruvisto committed rAFP05fc02919a74: new entry: Commuting_Hermitian.
new entry: Commuting_Hermitian
Aug 23 2022, 9:32 AM

Jul 20 2022

pruvisto committed rAFP0070374b7d4e: XZ compression for Safe_Distance examples (safes 160 MB!).
XZ compression for Safe_Distance examples (safes 160 MB!)
Jul 20 2022, 8:42 PM

Jul 18 2022

pruvisto committed rAFP74eeeedd2e19: ORCID for Manuel Eberl.
ORCID for Manuel Eberl
Jul 18 2022, 4:30 PM
pruvisto committed rAFP986cca9bb908: name change for Kądziołka.
name change for Kądziołka
Jul 18 2022, 4:15 PM
pruvisto committed rAFPe9b11372f955: name change for Kądziołka.
name change for Kądziołka
Jul 18 2022, 2:20 PM

May 10 2022

pruvisto committed rAFPb8c4aec14ebf: updated name and email address of Rose Bohrer.
updated name and email address of Rose Bohrer
May 10 2022, 1:24 AM

May 9 2022

pruvisto committed rAFP4ef570cafca9: updated name and email address of Rose Bohrer.
updated name and email address of Rose Bohrer
May 9 2022, 3:38 PM

Nov 16 2021

pruvisto committed rISABELLE227915e07891: more material for HOL-Analysis.Infinite_Sum.
more material for HOL-Analysis.Infinite_Sum
Nov 16 2021, 9:57 PM
pruvisto committed rAFP7aec7688b019: adapted to new version of Infinite_Sum in isabelle-dev.
adapted to new version of Infinite_Sum in isabelle-dev
Nov 16 2021, 12:00 AM

Nov 14 2021

pruvisto committed rAFP271732661ef5: changed affiliation of eberl (this time properly).
changed affiliation of eberl (this time properly)
Nov 14 2021, 4:10 AM
pruvisto committed rAFPc936740f4927: changed affiliation of Eberl.
changed affiliation of Eberl
Nov 14 2021, 4:10 AM

Nov 9 2021

pruvisto committed rAFP0051ace7ae35: changed affiliation of eberl (this time properly).
changed affiliation of eberl (this time properly)
Nov 9 2021, 3:53 PM
pruvisto committed rAFPfb912ad7a64c: changed affiliation of eberl.
changed affiliation of eberl
Nov 9 2021, 3:42 PM

Oct 19 2021

pruvisto committed rAFP7a08c3aec8d9: updated website/email address.
updated website/email address
Oct 19 2021, 4:17 PM
pruvisto committed rISABELLEd592354c4a26: removed some 'private' modifiers from HOL-Computational_Algebra.
removed some 'private' modifiers from HOL-Computational_Algebra
Oct 19 2021, 4:10 PM
pruvisto committed rISABELLEee039c11fb6f: updated email address.
updated email address
Oct 19 2021, 4:10 PM

Oct 7 2021

pruvisto committed rAFPf8ba1eaa5cec: adapted QHLProver to isabelle-dev/409ca22dee4c.
adapted QHLProver to isabelle-dev/409ca22dee4c
Oct 7 2021, 10:21 PM
pruvisto committed rAFPd6153e63e6cb: adapted to isabelle-dev/409ca22dee4c.
adapted to isabelle-dev/409ca22dee4c
Oct 7 2021, 12:59 PM
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
Oct 7 2021, 12:58 PM

Jul 26 2021

pruvisto committed rAFPfdc94d7251ed: Added Finitely_Generated_Abelian_Groups to metadata.
Added Finitely_Generated_Abelian_Groups to metadata
Jul 26 2021, 10:34 PM

Jul 7 2021

pruvisto committed rAFP9c417896a51d: Added missing Public_Announcement_Logic to ROOTS file.
Added missing Public_Announcement_Logic to ROOTS file
Jul 7 2021, 9:48 PM

May 27 2021

pruvisto committed rAFPcddbe565783d: sitegen for Padic_Ints.
sitegen for Padic_Ints
May 27 2021, 11:31 PM
pruvisto committed rAFPf463e6d25245: new entry: Padic_Ints.
new entry: Padic_Ints
May 27 2021, 11:31 PM

Apr 7 2021

pruvisto committed rISABELLE56db8559eadb: fixed problematic addition operation in the 'approximation' package (previous….
fixed problematic addition operation in the 'approximation' package (previous…
Apr 7 2021, 5:31 PM
pruvisto committed rAFPc81dd066bd29: adapted to isabelle-dev/56db8559eadb.
adapted to isabelle-dev/56db8559eadb
Apr 7 2021, 5:31 PM

Mar 3 2021

pruvisto committed rAFPf29eeda4f519: Tuned presentation of Buffon's needle.
Tuned presentation of Buffon's needle
Mar 3 2021, 10:39 PM

Feb 19 2021

pruvisto committed rISABELLEf6bb31879698: HOL-Analysis/Probability: Hoeffding's inequality, negative binomial….
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial…
Feb 19 2021, 7:36 PM
pruvisto committed rAFP547cd5ffe43f: adapted to isabelle-dev/73253:f6bb31879698.
adapted to isabelle-dev/73253:f6bb31879698
Feb 19 2021, 7:28 PM

Feb 18 2021

pruvisto committed rAFP3ce2153720f3: Buffons_Needle: tuned presentation.
Buffons_Needle: tuned presentation
Feb 18 2021, 6:46 PM
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 18 2021, 6:46 PM

Feb 11 2021

pruvisto committed rAFP4b1c5705378b: Ergodic_Theory: tuned some names.
Ergodic_Theory: tuned some names
Feb 11 2021, 6:07 AM
pruvisto committed rAFP24b6785e3e55: Ergodic_Theory: ergodicity of the shift operator.
Ergodic_Theory: ergodicity of the shift operator
Feb 11 2021, 6:07 AM

Feb 10 2021

pruvisto committed rAFPa2632f50a689: Ergodic_Theory: tuned some names.
Ergodic_Theory: tuned some names
Feb 10 2021, 5:54 PM
pruvisto committed rAFP539ea87e2f86: Ergodic_Theory: ergodicity of the shift operator.
Ergodic_Theory: ergodicity of the shift operator
Feb 10 2021, 5:07 PM

Feb 2 2021

pruvisto committed rAFPb4869ef2d1ca: fixed category for Blue_Eyes.
fixed category for Blue_Eyes
Feb 2 2021, 10:53 PM
pruvisto added a reverting change for rAFP4450302adc70: fixed category for Blue_Eyes: rAFP357a81dcd962: Backed out changeset 4450302adc70.
Feb 2 2021, 10:53 PM
pruvisto committed rAFP357a81dcd962: Backed out changeset 4450302adc70.
Backed out changeset 4450302adc70
Feb 2 2021, 10:53 PM
pruvisto committed rAFP4450302adc70: fixed category for Blue_Eyes.
fixed category for Blue_Eyes
Feb 2 2021, 10:53 PM
pruvisto committed rAFP17c110a297d8: New entry: Blue_Eyes.
New entry: Blue_Eyes
Feb 2 2021, 10:53 PM
pruvisto committed rAFPd5d57c1027c0: sitegen for Blue_Eyes.
sitegen for Blue_Eyes
Feb 2 2021, 10:53 PM

Jan 13 2021

pruvisto committed rAFPdd8e0cdca49e: sitegen for CSP_RefTK.
sitegen for CSP_RefTK
Jan 13 2021, 12:38 AM
pruvisto committed rAFP626c957d2647: New submission: CSP_RefTK.
New submission: CSP_RefTK
Jan 13 2021, 12:38 AM

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 9 2021, 3:56 PM

Jan 8 2021

pruvisto committed rAFP03248eeafe63: Algebraic_Numbers: some material on algebraic integers.
Algebraic_Numbers: some material on algebraic integers
Jan 8 2021, 10:12 PM
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
Jan 8 2021, 10:12 PM
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 8 2021, 10:12 PM

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
Jan 5 2021, 3:36 AM
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 5 2021, 2:25 AM

Jan 4 2021

pruvisto committed rAFPdfe83cc412a3: adapted to isabelle-dev/74be162a47cd.
adapted to isabelle-dev/74be162a47cd
Jan 4 2021, 8:58 PM
pruvisto committed rISABELLE7ad9f197ca7e: HOL-Complex_Analysis: coefficient asymptotics for meromorphic functions.
HOL-Complex_Analysis: coefficient asymptotics for meromorphic functions
Jan 4 2021, 8:55 PM
pruvisto committed rISABELLEab9e27da0e85: HOL-Library: Changed notation for sum_mset.
HOL-Library: Changed notation for sum_mset
Jan 4 2021, 8:55 PM

Sep 8 2020

pruvisto committed rAFP858b1818bdf7: sitegen for PAC_Checker.
sitegen for PAC_Checker
Sep 8 2020, 7:15 AM
pruvisto committed rAFP67db0fea0947: new entry PAC_Checker.
new entry PAC_Checker
Sep 8 2020, 7:15 AM

Aug 26 2020

pruvisto committed rAFPfd19c62b5416: sitegen for Ordinal_Partitions.
sitegen for Ordinal_Partitions
Aug 26 2020, 2:44 PM
pruvisto committed rAFP367cebefeee8: New entry: Ordinal_Partitions.
New entry: Ordinal_Partitions
Aug 26 2020, 2:44 PM
pruvisto committed rAFP6e56f286a19f: sitegen for Amicable_Numbers.
sitegen for Amicable_Numbers
Aug 26 2020, 2:44 PM
pruvisto committed rAFP4bc297a7a99a: New entry: Amicable_Numbers.
New entry: Amicable_Numbers
Aug 26 2020, 2:44 PM

Jun 26 2020

pruvisto committed rAFP95f6b086f304: added missing HTML file.
added missing HTML file
Jun 26 2020, 3:49 AM
pruvisto committed rAFPcd2ad55be677: new entry Nash_Williams.
new entry Nash_Williams
Jun 26 2020, 3:49 AM
pruvisto committed rAFPd52fe24a2f10: sitegen for Nash_Williams.
sitegen for Nash_Williams
Jun 26 2020, 3:49 AM

May 17 2020

pruvisto committed rAFPa96e67c30c51: sitegen for Matrices_for_ODEs.
sitegen for Matrices_for_ODEs
May 17 2020, 10:41 AM
pruvisto committed rAFPbe5001e48d96: New entry: Matrices_for_ODEs.
New entry: Matrices_for_ODEs
May 17 2020, 10:41 AM
pruvisto committed rAFP86469b8ab86e: New entry LTL_Normal_Form.
New entry LTL_Normal_Form
May 17 2020, 10:41 AM
pruvisto committed rAFP1421ffc83ad1: sitegen for LTL_Normal_Form.
sitegen for LTL_Normal_Form
May 17 2020, 10:41 AM
pruvisto committed rAFPd7605a61179d: Fixed missing MathJax fonts.
Fixed missing MathJax fonts
May 17 2020, 10:40 AM

May 15 2020

pruvisto committed rAFP231c5cb952ed: adapted to isabelle-dev/07c85c68ff03.
adapted to isabelle-dev/07c85c68ff03
May 15 2020, 11:41 AM
pruvisto committed rISABELLE07c85c68ff03: added missing preprocessing step for extraction (due to Stefan Berghofer).
added missing preprocessing step for extraction (due to Stefan Berghofer)
May 15 2020, 11:41 AM
pruvisto committed rISABELLEdb120661dded: new HOL simproc: eliminate_false_implies.
new HOL simproc: eliminate_false_implies
May 15 2020, 11:41 AM

May 14 2020

pruvisto committed rISABELLE8ed78bb0b915: Tuned some proofs in HOL-Analysis.
Tuned some proofs in HOL-Analysis
May 14 2020, 2:59 PM

May 13 2020

pruvisto committed rISABELLE5656ec95493c: generalised pigeonhole principle in HOL-Library.FuncSet.
generalised pigeonhole principle in HOL-Library.FuncSet
May 13 2020, 5:36 PM
pruvisto committed rISABELLEdca11678c495: new constant power_int in HOL.
new constant power_int in HOL
May 13 2020, 5:36 PM
pruvisto committed rISABELLEc095d3143047: New HOL simproc 'datatype_no_proper_subterm'.
New HOL simproc 'datatype_no_proper_subterm'
May 13 2020, 5:36 PM
pruvisto committed rAFP24488f2caddd: adapted to isabelle-dev/c095d3143047.
adapted to isabelle-dev/c095d3143047
May 13 2020, 5:35 PM

May 4 2020

pruvisto committed rAFPdfe61dcb44e3: Backed out changeset c78f358a496d.
Backed out changeset c78f358a496d
May 4 2020, 9:57 PM
pruvisto added a reverting change for rAFPc78f358a496d: Adapted to isabelle-dev/159e33bdddc6: rAFPdfe61dcb44e3: Backed out changeset c78f358a496d.
May 4 2020, 9:57 PM
pruvisto committed rAFP62197b3a4d53: More robust proof in Slicing.
More robust proof in Slicing
May 4 2020, 9:01 PM
pruvisto committed rAFPc78f358a496d: Adapted to isabelle-dev/159e33bdddc6.
Adapted to isabelle-dev/159e33bdddc6
May 4 2020, 9:01 PM
pruvisto committed rAFP95ddcc9a71a2: More robust apply proofs in Finger-Trees.
More robust apply proofs in Finger-Trees
May 4 2020, 9:01 PM
pruvisto committed rAFP3506cde43185: Extended Stirling's formula to complex numbers.
Extended Stirling's formula to complex numbers
May 4 2020, 9:01 PM

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
Apr 29 2020, 5:25 AM
pruvisto committed rAFP573f2cf3cd36: Tuned MathJax templates.
Tuned MathJax templates
Apr 29 2020, 5:25 AM
pruvisto committed rAFP42e714e75928: Added MathJax support for abstracts.
Added MathJax support for abstracts
Apr 29 2020, 5:25 AM
pruvisto committed rAFP263550b73c79: Documentation for MathJax.
Documentation for MathJax
Apr 29 2020, 5:25 AM
pruvisto committed rAFP22f31d772be8: Another attempt to fix MathJax on Jenkins 2.
Another attempt to fix MathJax on Jenkins 2
Apr 29 2020, 5:25 AM
pruvisto committed rAFPeb0a838f7b0d: Another attempt to fix MathJax on Jenkins.
Another attempt to fix MathJax on Jenkins
Apr 29 2020, 5:25 AM
pruvisto committed rAFP95969655d4f0: Trying to fix strange sitegen problem with Jenkins.
Trying to fix strange sitegen problem with Jenkins
Apr 29 2020, 5:25 AM
pruvisto committed rAFP6b713b029127: Fixed typo in abstract of Lucas_Theorem.
Fixed typo in abstract of Lucas_Theorem
Apr 29 2020, 5:25 AM
pruvisto committed rAFPdfe1da9bee38: sitegen for Lucas_Theorem.
sitegen for Lucas_Theorem
Apr 29 2020, 5:25 AM
pruvisto committed rAFP9fdc17973d24: new entry Lucas_Theorem.
new entry Lucas_Theorem
Apr 29 2020, 5:25 AM

Apr 25 2020

pruvisto added a reverting change for rAFP9af08c18b665: Switched to MathJax CDN to diagnose Safari issues: rAFP6c95b5484a25: Backed out changeset 9af08c18b665.
Apr 25 2020, 12:34 PM
pruvisto committed rAFP6c95b5484a25: Backed out changeset 9af08c18b665.
Backed out changeset 9af08c18b665
Apr 25 2020, 12:34 PM
pruvisto committed rAFP9af08c18b665: Switched to MathJax CDN to diagnose Safari issues.
Switched to MathJax CDN to diagnose Safari issues
Apr 25 2020, 11:59 AM