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

proper quoting of paths in MaSh shell script, take 2 (cf. b00eeb8e352e)

added "fact_filter" option to Mirabelle

tweak SPASS default a tiny bit, so that a more interesting heuristic is chosen when "slicing=false" (for experiments)

some notes on the Isabelle component repository at TUM;

use filterlim in Lim and SEQ; tuned proofs

conversion rules for at, at_left and at_right; applied to l'Hopital's rules.

weakened assumptions for lhopital_right_0

tuned proof

add L'Hôpital's rule

add filterlim rules for exp and ln to infinity

add filterlim rules for inverse and at_infinity

add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image

add filterlim rules for unary minus and inverse