proper build_graph to make session selection work as in "isabelle build";

incorporate sessions with record_proofs;

clarified options;

clarified signature;

clarified signature;

clarified signature;

clarified signature;

clarified "isabelle update" options -- more like "isabelle dump";

clarified treatment of base logic image;

simplified options: always split;

proper guard -- avoid bad result;

split into standard partitions, for improved scalability;

clarified defaults;

tuned signature;

clarified signature: static Dump.Context vs. dynamic Dump.Session;

tuned signature;

tuned signature;

clarified sessions/directories;

clarified signature default;

clarified signature default;

more operations for type classes;

setup preprocessing for HOL proofs;

support preprocessing of exported proofs;

early setup of proof preprocessing;

clarified output and input of Typ/Term;

adapted to ML version;

more compact XML;

more compact XML: separate environment for free variables; clarified fold_proof_terms vs. fold_proof_terms_types;

more compact XML;

merged

proper ML names;

clarified standard_proof_of: prefer expand_proof over somewhat adhoc strip_thm_proof;

some treatment of OfClass proofs;

tuned signature;

misc tuning and clarification;

proper treatment of axm_proof/oracle_proof like a closed proof constant, e.g. relevant for proof reconstruction of List.list.full_exhaustive_list.simps;

clarified oracle_proof;

tuned;

tuned;

tuned;

clarified signature;

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;