New theorems to enable the simplification of certain functions when applied to specific natural number constants (such as 4)

removed Kleene_Algebra because of superior AFP entry; authors agreed

typo

uniform treatmen of result

tuned variable names

more generous max number of suggestions, for more safety

changed MaSh to use SML version instead of Python version of naive Bayes by default (i.e. if MASH=yes in the settings, or 'fact_filter=mash' with no other explicit setting)

export more ML functions, for experimentation

tuned signature;

disabled IDF for now -- empirical evidence points the wrong way (as usual)

tuning

tuning

optimized computation

enabled IDF for naive Bayes ML

tuning

repaired subscript problem in SML kNN

tuning

always remove duplicates in meshing + use weights for Naive Bayes

updated naive Bayes

don't generate discriminators and selectors for 'datatype_new' unless the user asked for it

don't conceal (co)datatypes

changed '-:' to 'dead' in BNF

got rid of '=:' squiggly

use '%x. x = C' as default discriminator for nullary constructor C, instead of relying on odd '=:' syntax

renamed 'MaSh' option

document '=:' syntax better

capitalize even more carefully (see 5ac67041ccf8), e.g. relevant for option "z3_non_commercial" and prospective "MaSh";

tuned;

clarified copy_file: allow to rename base name, e.g. relevant for 'display_drafts';

support for regular Windows TeX installation;