new material on eqiintegrable functions, etc.

clarified treatment of individual theorems; tuned messages;

tuned signature;

clarified signature;

clarified derivation_name vs. raw_derivation_name;

merged

more careful treatment of hidden type variable names: smash before zero_var_indexes to get standard enumeration;

more careful treatment of standard_vars: rename apart from existing frees and avoid approximative Name.declared, proper application of unvarifyT within terms of proof;

support Export_Theory.read_proof, based on theory_name and serial;

clarified PThm: theory_name simplifies retrieval from exports;

Indexname.toString according to string_of_vname' in ML;

clarified type Indexname, with plain value Int; eliminated pointless cache_int;

more complete pattern match;

export facts with reconstructed proof term (if possible), but its PThm boxes need to be collected separately;

support for (fully reconstructed) proof terms in Scala; proper cache_typs;

new material; rotated premises of Lim_transform_eventually

clarified name context for abstractions -- in contrast to 367e60d9aa1b and Term.variant_frees (*as they are printed :-*);

tuned;

uniform standard_vars for terms and proof terms;

treat simproc results as atomic -- more compact proof terms;

tuned;

minor performance tuning;

NEWS and example for Theory.join_theory;

tuned whitespace;

more compact proof terms;

more documentation;

added SUBPROOFS / "subproofs" method combinator, for more compact proofterms;

clarified modules;

merged

more compact proof terms;

more robust -- notably for metis, which tends to accumulate tpairs;

tuned -- avoid shadowing of ML names;

tuned;

more compact proof terms;

tuned;

tuned;

tuned -- eliminated unused parameters;

more direct/compact export of proof terms;

output physical_stderr, e.g. for low-level debugging;

tuned;

do not open ML structures;

tuned;

misc tuning -- slightly more readable;

simplified defs (thanks to Mohammad)

record sort constraints unconditionally: minimal performance implications;

more careful export of unnamed proof boxes: avoid duplicates via memoing;

tuned signature;

export each PThm node separately: slightly more scalable;

allow duplicate exports via strict = false;

tuned message;

more positions;

more positions;

tuned;

formal position for PThm nodes;

clarified ML types;

proper treatment of body oracles, outside of recursion into thms graph;

prefer named lemmas -- more compact proofterms;

prefer named lemmas -- more compact proofterms;

tuned whitespace -- slightly more readable;

clarified signature: fewer warnings in ML IDE;