clarified identity of PThm nodes: do not reuse old id after renaming -- enforce uniqueness of substructures;

clarified signature;

Fixed brace matching (plus some whitespace cleanup)

merged

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;