PIDE reports of implicit variable scope;

tuned;

Probability: simplified Levy's uniqueness theorem

avoid reference to invisible theorem, by using another one instead (suggested by Anders Schlichtkrull; the document's author is incomunicado)

tuning

typo (reported by Anders Schlichtkrull)

simplified proof for measurability of isCont

instantiate multiset with multiset ordering

more accurate total timing

merged

tuned

merged

NEWS;

clarified positions, e.g. for reports on literal facts;

tuned whitespace;

tuned;

tuned;

spelling

combinator to build partial equivalence relations from a predicate and an equivalenc relation

default one-step rules for predicates on relations; clarified status of legacy input abbreviations

basic facts about almost everywhere fix bijections

dedicated locale for total bijections

tuned sections

relating gbinomial and binomial, still using distinct definitions

clarified fact position, notably for reports on literal facts;

more accurate facts index;

tuned signature;

tuned signature;

simplified definitions of combinatorial functions

define binomial coefficents directly via combinatorial definition