cleaned up more messy proofs

merged

cleaned up some messy proofs

tuned

replaced bad example

polished some ancient proofs

merged

Simplified, tidied and generalised proofs esp of Binomial Theorem.

more uniform / rigid checking of Goal.prove_common vs. Proof.conclude_goal -- NB: Goal.prove_common cannot check hyps right now, e.g. due to undeclared Simplifier prems;

more accurate goal context;

tuned;

more accurate goal context; actually check assertions;

more official option;

clarified node edits sent to prover -- Clear/Blob only required for text edits within editor;

exclude gzipped files from document model, to avoid confusion about actual file name and content;

more .hgignore;

tuned messages;

more total master_directory -- NB: this is used outside command transactions (see also 92961f196d9e);

correctly account for dead variables when naming set functions

compile

rationalize imports

eliminated Sledgehammer's dependency on old-style datatypes

moved meson up the dependency chain

moving 'Order_Relation' to 'HOL' (since it's a BNF dependency)