Page MenuHomeIsabelle/Phabricator

pruvisto (Manuel Eberl)
User

Projects

User Details

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

Recent Activity

Tue, Sep 8

pruvisto committed rAFP858b1818bdf7: sitegen for PAC_Checker.
sitegen for PAC_Checker
Tue, Sep 8, 7:15 AM
pruvisto committed rAFP67db0fea0947: new entry PAC_Checker.
new entry PAC_Checker
Tue, Sep 8, 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
pruvisto committed rISABELLE8b8f9d3b3fac: Simplified Harmonic_Numbers.
Simplified Harmonic_Numbers
Dec 2 2019, 11:13 AM
pruvisto committed rISABELLE954ee5acaae0: Split off new HOL-Complex_Analysis session from HOL-Analysis.
Split off new HOL-Complex_Analysis session from HOL-Analysis
Dec 2 2019, 11:13 AM
pruvisto committed rAFPe30fe5fba4d7: Merged.
Merged
Dec 2 2019, 11:12 AM
pruvisto committed rAFP4f482d20a008: adapted to isabelle-dev 954ee5acaae0.
adapted to isabelle-dev 954ee5acaae0
Dec 2 2019, 11:12 AM