Page MenuHomeIsabelle/Phabricator

pruvisto (Manuel Eberl)
User

Projects

User Details

User Since
Nov 19 2019, 1:16 PM (95 w, 6 d)

Recent Activity

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

Apr 22 2020

pruvisto committed rAFP9792b8607ad6: Tuned MathJax templates.
Tuned MathJax templates
Apr 22 2020, 6:28 PM
pruvisto committed rAFP2d9943b949f2: 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 22 2020, 6:17 PM
pruvisto committed rAFP40282cc15d5e: Documentation for MathJax.
Documentation for MathJax
Apr 22 2020, 5:12 PM
pruvisto committed rAFP9de2c007f193: Another attempt to fix MathJax on Jenkins 2.
Another attempt to fix MathJax on Jenkins 2
Apr 22 2020, 1:36 PM
pruvisto committed rAFPefc17bf0ebff: Another attempt to fix MathJax on Jenkins.
Another attempt to fix MathJax on Jenkins
Apr 22 2020, 1:22 PM
pruvisto committed rAFPabea6d387938: Trying to fix strange sitegen problem with Jenkins.
Trying to fix strange sitegen problem with Jenkins
Apr 22 2020, 12:38 PM
pruvisto committed rAFPb589d11dec72: Sitegen with MathJax.
Sitegen with MathJax
Apr 22 2020, 12:06 PM
pruvisto committed rAFPfd3862d57fdf: Added MathJax support for abstracts.
Added MathJax support for abstracts
Apr 22 2020, 12:06 PM

Mar 28 2020

pruvisto committed rAFP81ec186eae5e: Fixed some typos in Furstenberg_Topology.
Fixed some typos in Furstenberg_Topology
Mar 28 2020, 12:15 PM

Mar 10 2020

pruvisto committed rISABELLE2aa38099aa8c: updated NEWS w.r.t. e0237f2eb49d.
updated NEWS w.r.t. e0237f2eb49d
Mar 10 2020, 2:18 PM

Feb 18 2020

pruvisto committed rAFPbf1920e1bc60: make Poincare_Disc build on Complex_Geometry.
make Poincare_Disc build on Complex_Geometry
Feb 18 2020, 12:10 PM
pruvisto committed rAFPc35f8cc3dda7: repaired broken proofs in Skip_Lists; removed unfinished experimental thy file.
repaired broken proofs in Skip_Lists; removed unfinished experimental thy file
Feb 18 2020, 12:01 PM

Feb 14 2020

pruvisto committed rAFP77a8004b99f4: sitegen for Arith_Prog_Rel_Primes.
sitegen for Arith_Prog_Rel_Primes
Feb 14 2020, 5:36 PM
pruvisto committed rAFPbd5ff2d92ffa: new entry Arith_Prog_Rel_Primes.
new entry Arith_Prog_Rel_Primes
Feb 14 2020, 5:36 PM
pruvisto committed rAFPa222e106ac18: added new entries: Complex_Geometry and Poincare_Disc.
added new entries: Complex_Geometry and Poincare_Disc
Feb 14 2020, 5:36 PM
pruvisto committed rAFPa4ca8d95843b: fixed incorrect HTML entity in Poincare_Disc metadata.
fixed incorrect HTML entity in Poincare_Disc metadata
Feb 14 2020, 5:36 PM
pruvisto committed rAFP1775f91f0787: Fixed broken citation in Poincare_Disc.
Fixed broken citation in Poincare_Disc
Feb 14 2020, 5:36 PM

Feb 12 2020

pruvisto committed rAFP0f0adba767a3: adapted to isabelle-dev/e0237f2eb49d.
adapted to isabelle-dev/e0237f2eb49d
Feb 12 2020, 10:57 PM

Jan 21 2020

pruvisto committed rISABELLEe0237f2eb49d: Removed multiplicativity assumption from normalization_semidom.
Removed multiplicativity assumption from normalization_semidom
Jan 21 2020, 11:58 PM

Jan 17 2020

pruvisto committed rISABELLEa3f7f00b4fd8: Removed unnecessary and problematic trivial lemma from HOL-Algebra.
Removed unnecessary and problematic trivial lemma from HOL-Algebra
Jan 17 2020, 10:26 PM

Jan 2 2020

pruvisto committed rAFP3c6cf3b9146b: More material for Zeta_Function: Hadjicostas's formula.
More material for Zeta_Function: Hadjicostas's formula
Jan 2 2020, 7:16 PM

Dec 20 2019

pruvisto committed rAFP88a82d6fdd30: Corrected name.
Corrected name
Dec 20 2019, 3:33 PM

Dec 3 2019

pruvisto committed rISABELLE6f8422385878: Removed orphaned theory from HOL-Analysis.
Removed orphaned theory from HOL-Analysis
Dec 3 2019, 5:15 PM
pruvisto committed rISABELLE6617fb368a06: Reorganised HOL-Complex_Analysis.
Reorganised HOL-Complex_Analysis
Dec 3 2019, 12:43 PM

Dec 2 2019

pruvisto committed rISABELLE777d673fa672: Removed duplicate theorems from HOL-Analysis.
Removed duplicate theorems from HOL-Analysis
Dec 2 2019, 4:17 PM
pruvisto committed rISABELLEa8ccea88b725: Flattened dependency tree of HOL-Analysis.
Flattened dependency tree of HOL-Analysis
Dec 2 2019, 4:17 PM
pruvisto committed rISABELLE6695aeae8ec9: Merged.
Merged
Dec 2 2019, 11:13 AM