basic wrapper for session build dialog;

tuned;

tuned signature in accordance to document operations;

tuned;

merged

\<noteq> now has the same associativity as ~= and =

tweaked order of theorems to avoid forward dependencies (MaSh)

rationalized MaSh evaluation harness

more robustness in the face of MaSh format changes -- don't overwrite new versions with old versions

added feature weights in MaSh

promote local facts using a hack (for MaSh)

proper action labels, to make this appear in the "Shortcuts" panel, for example;

turned off noisy MaSh features

added MaSh learning to Mirabelle

fixed bug in initialization of naive Bayes (MaSh)

tuned MaSh exporter -- and don't make temp directories unless explicitly told so

generalized MaSh exporter to sets of theories

remove SMT proofs in Multivariate_Analysis

prove tendsto_power_div_exp_0 * * * missing rename

add filterlim rules for eventually monotone bijective functions; mirror rules for at_top, at_bot; apply them to prove convergence of arctan at infinity and tan at pi/2

merged

emit bulk edits on initialization of multiple buffers, which greatly improves performance when starting big sessions (e.g. JinjaThreads);

go back to Z3 3.2

tuned defs of sec_xyz

provide general insert_line_padding as convenience operation, e.g. for BeanShell macros;

simplify MaSh term patterns + add missing global facts if there aren't too many

MaSh improvements: deeper patterns + more respect for chained facts

tuned names

tweaked MaSh exporter

renamed "Type.thy" to something that's less likely to cause conflicts