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

fixed broken abstract for PAPP_Impossibility

sitegen for Padic_Field

sitegen for Risk_Free_Lending

new entry: Padic_Field

new entry: Risk_Free_Lending

sitegen for Number_Theoretic_Transform

fixed metadata for Hales_Jewett

new entry Number_Theoretic_Transform

sitegen for Commuting_Hermitian

new entry: Commuting_Hermitian

XZ compression for Safe_Distance examples (safes 160 MB!)

ORCID for Manuel Eberl

name change for Kądziołka

name change for Kądziołka

updated name and email address of Rose Bohrer

updated name and email address of Rose Bohrer

more material for HOL-Analysis.Infinite_Sum

adapted to new version of Infinite_Sum in isabelle-dev

changed affiliation of eberl (this time properly)

changed affiliation of Eberl

changed affiliation of eberl (this time properly)

changed affiliation of eberl

updated website/email address

removed some 'private' modifiers from HOL-Computational_Algebra

updated email address

adapted QHLProver to isabelle-dev/409ca22dee4c

adapted to isabelle-dev/409ca22dee4c

new notion of infinite sums in HOL-Analysis, ordering on complex numbers

Added Finitely_Generated_Abelian_Groups to metadata

Added missing Public_Announcement_Logic to ROOTS file

sitegen for Padic_Ints

new entry: Padic_Ints

fixed problematic addition operation in the 'approximation' package (previous…

adapted to isabelle-dev/56db8559eadb

Tuned presentation of Buffon's needle

HOL-Analysis/Probability: Hoeffding's inequality, negative binomial…

adapted to isabelle-dev/73253:f6bb31879698

Buffons_Needle: tuned presentation

Ergodic_Theory: removed 'pullback_algebra'. Turns out it already exists and is…

Ergodic_Theory: tuned some names

Ergodic_Theory: ergodicity of the shift operator

Ergodic_Theory: tuned some names

Ergodic_Theory: ergodicity of the shift operator

fixed category for Blue_Eyes

Backed out changeset 4450302adc70

fixed category for Blue_Eyes

New entry: Blue_Eyes

sitegen for Blue_Eyes

sitegen for CSP_RefTK

New submission: CSP_RefTK

Corrected lemma that was too specific in HOL-Computational_Algebra

Algebraic_Numbers: some material on algebraic integers

some algebra material for HOL: characteristic of a ring, algebraic integers

HOL-Data_Structures: added Selection and time functions for list functions

HOL-Library.Multiset: new notation for prod_mset, consistent with sum_mset

adapted to isabelle-dev/74be162a47cd: added some renamings that were missed…

adapted to isabelle-dev/74be162a47cd

HOL-Complex_Analysis: coefficient asymptotics for meromorphic functions

HOL-Library: Changed notation for sum_mset

sitegen for PAC_Checker

new entry PAC_Checker

sitegen for Ordinal_Partitions

New entry: Ordinal_Partitions

sitegen for Amicable_Numbers

New entry: Amicable_Numbers

added missing HTML file

new entry Nash_Williams

sitegen for Nash_Williams

sitegen for Matrices_for_ODEs

New entry: Matrices_for_ODEs

New entry LTL_Normal_Form

sitegen for LTL_Normal_Form

Fixed missing MathJax fonts

adapted to isabelle-dev/07c85c68ff03

added missing preprocessing step for extraction (due to Stefan Berghofer)

new HOL simproc: eliminate_false_implies

Tuned some proofs in HOL-Analysis

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

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

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