Library/Tree: bst is preferred to be a function

Library/Tree: use datatype_new, bst is an inductive predicate

more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs

import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure

some lemmas about the indicator function; removed lemma sums_def2

generate type correct terms in uncheck phase

updated to sumatra_pdf-2.5.2;

ProofGeneral-4.2-2 is optional component (including the traditional helper scripts);

removed obsolete Isar system commands -- raw ML console is normally used for system tinkering;

tuned comments;

updated README;

"isabelle tty" is superseded by "isabelle console";

tuned description: fit into 80 chars terminal;

qualified String.explode and String.implode

removed non-existing MaSh component from list

modernized diagnostic options

use SMT2

compile

tuning

killed Python version of MaSh, now that the SML version works adequately

tracing facilities for the code generator preprocessor

tuned interface

corrected handled exception

proper trading of variables; more appropriate ML variable names

modernized

jedit_completion_immediate is enabled by default: let all users participate in slightly more ambitious symbol insertion;

removed slightly odd fall-back on complete-word (NB: connection to default menu action is unclear);

updated NEWS -- removed material that is already in the manual;