clarified signature: prefer total operations;

proper graph traversal: avoid multiple visit of unnamed nodes;

more scalable: avoid huge intermediate XML elems;

more scalable buffer: produce compact chunks on the fly, avoid too many small particles that might congest heap management;

NEWS;

merged

export thm_deps;

proper theory context;

clarified thm_id vs. thm_node/thm: retain theory_name; support for thm_deps: expand unnamed nodes;

clarified signature;

tuned;

unused (see 095dadc62bb5);

tuned;

tuned signature;

clarified modules;

clarified modules;

tuned;

clarified signature;

tuned

tuned

merged

tuned

merged

clarified signature;

clarified export of axioms and theorems (identified derivations instead of projected facts);

tuned signature;

back to uniform serial (reverting 913b4afb6ac2): this allows to treat derivation id like name space entity id;

module Thm_Name for Isabelle/Scala;

tuned;

clarified modules;

tuned;

tuned

tuned names

clarified signature;

discontinued peek_status: unused and not clearly defined;

more documentation on oracles;

proper theory context for global props;

more thorough check, using full dependency graph of finished proofs;

added ML antiquotation @{oracle_name};

more robust, notably for open_proof of unnamed derivation;

tuned comments;

NEWS;

more accurate proposition for cheat_tac (command 'sorry');

added command 'thm_oracles';

clarified type for recorded oracles;

unused;

clarified signature;

clarified modules;

clarified lookup operations: more scalable for multiple retrieval;

clarified signature;

merged

maintain thm_name vs. derivation_id for global facts;

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;

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;