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;

tuned;

prefer named lemmas -- more compact proofterms;

more compact proofterms;

eliminated pointless comments;

clarified proofterms;

more robust and convenient treatment of implicit context;

removed junk (cf. fa933b98d64d);

explicit check of left-over constraints from different theory, e.g. due to lack of Thm.trim_context;

more careful treatment of implicit context;

more careful treatment of implicit context;

proper build options;

merged

backed out changeset 1b8858f4c393: odd problems e.g. in CAVA_LTL_Modelchecker;

more careful treatment of implicit context;

clarified signature; more careful treatment of implicit context;