fix typo in Nitpick manual

optimized Nitpick's encoding and rendering of datatypes whose constructors don't appear in the problem

clean Nitpick's wellfoundedness cache once in a while, to avoid potential memory leak

renamed Nitpick option "coalesce_type_vars" to "merge_type_vars" (shorter) and cleaned up old hacks that are no longer necessary

eliminated some old uses of cumulative prems (!) in proof methods;

eliminated some unused/obsolete Args.bang_facts;

modernized structure Theory_Target;

removed unused Quickcheck_RecFun_Simps;

define simprocs: do not apply target_morphism prematurely, this is already done in LocalTheory.declaration;

bang_facts: legacy feature;

tuned proofs;

removed obsolete name_of -- cf. decode;

desymbolize: use Symbol.decode directly; recovered coding conventions of this file;

try SAT_Examples last, to minimize impact of global side-effects;

home-grown pretty printer for term -- Poly/ML 5.3.0 does not observe infix status of constructors (notably $);

Inserted missing theory dependency

merged

Merged.

Removed obsolete code.

updated to official Poly/ML 5.3.0;

switched some isatest sessions to official Poly/ML 5.3.0;

setup for official Poly/ML 5.3.0, which is now the default;

locale_const/target_notation: uniform use of Term.aconv_untyped; target_notation: pass on transformed term formally; removed obsolete Type.similar_types;

eliminated hard tabulators;

fixed some inappropriate names

merged

New theory Probability/Borel.thy, and some associated lemmas

merged

tuned error messages; tuned code

follow standard theory merge behaviour: do not change already selected solver