clarified keywords;

more indentation for quasi_command keywords;

tuned;

tuned;

tuned;

support for quasi_command keywords;

tuned signature: more uniform Keyword.spec;

indentation in reminiscence to Proof General (see proof-indent.el);

tuned;

tuned;

tuned;

clarified signature;

more operations;

clarified modules;

basic setup for indentation;

tuned;

more operations;

tuned

more lemmas to emphasize {0::nat..(<)n} as canonical representation of intervals on nat * * * more rules for setsum, setprod on intervals

avoid to hide equality behind (output) abbreviation

default rule for single-step reasoning

new style dummy_pats

added path_len

merged

got rid of class cmp; added height-size proofs by Daniel Stuewe

more instantiations for multiset

moved lemmas and locales around (with minor incompatibilities)

updated example

leverage new 'order' type class instantiation in multiset

updated examples

merged

misc tuning and modernization;

proper signature;

tuned signature;

simplify build scripts

misc tuning and modernization;

more antiquotations;

tuned;

merged

PIDE reports of implicit variable scope;

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;