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

rename filter_lim to filterlim to be consistent with filtermap

add check to Cooper's algorithm that left-hand of dvd is a numeral

merged

robust writing of MaSh state -- better drop learning data than cause other problems in Sledgehammer

avoid odd warnings due to failure of systray icon;

synchronized read access to cache file -- avoid potential conflict with ongoing write (which is non-atomic); clarified signature -- cache init is unsynchronized and hopefully used at most once per file;