add rule deflation_ID to proof script for take + constructor rules

more robust record syntax: use Type.raw_match to ignore sort constraints as in regular abbreviations (also note that constraints only affect operations, not types);

HOL record: explicitly allow sort constraints;

misc tuning and simplification;

explicit ProofContext.check_tfree;

merged

Respectfullness and preservation of list_rel

replaced slightly odd Typedecl.predeclare_constraints by plain declaration of type arguments -- also avoid "recursive" declaration of type constructor, which can cause problems with sequential definitions B.foo = A.foo; simplified via ProofContext.check_tfree;

get_sort: suppress dummyS from input; added check_tvar, check_tfree convenience; tuned;

modernized treatment of sort constraints in specification; pass-through type variables as usual as (string * sort) internally -- recovers proper sort handling;

typecopy: observe given sort constraints more precisely;

inline old Record.read_typ/cert_typ; spelling;

spelling;

theory RBT with abstract type of red-black trees backed by implementation RBT_Impl

tuned whitespace;

merged

merged

added "overlord" option (to get easy access to output files for debugging) + systematically use "raw_goal" rather than an inconsistent mixture

make Sledgehammer "minimize" output less confusing + round up (not down) time limits to nearest second

make Sledgehammer's "timeout" option work for "minimize"

fixed handling of "sledgehammer_params" that get a default value from Isabelle menu; and added "atp" as alias for "atps"

Spelling error: theroems -> theorems

advertise [rename_abs] attribute in LaTeXsugar -- wish I had known about this earier.

record package: corrected sort handling in type translations to avoid crashes when default sort is changed. Test case: record 'a T = elem :: 'a defaultsort order term elem (* low-level exception *)