tuned signature;

more compact XML representation;

proper generalize_proof: schematic variables need to be explicit in the resulting proof term (for shrink/reconstruct operation);

tuned;

tuned -- more direct ML expressions;

clarified modules;

tuned whitespace;

more accurate treatment of propositions within proof terms, but these are ultimately ignored for performance reasons;

unused;

document antiquotations + clarify porting text slightly

updated veriT part of Sledgehammer documentation

added para constrasting 'primrec' and 'fun' -- and removed my middle name

dedicated fact collections for algebraic simplification rules potentially splitting goals

merged

tuned;

misc tuning and clarification;

tuned;

tuned -- allow slightly more expensive atomic proofs;

clarified signature -- some operations to support fully explicit proof terms;

tuned;

tuned;

proper treatment of sorts;

tuned app_types: more direct map_proof_types_same;

tuned;

generalized parsing, for e.g. Leo-III

More theorems about limits, including cancellation simprules

Generalised two results concerning limits from the real numbers to type classes

formally augmented corresponding rules for field_simps