tuned;

tuned names;

more operations; more accurate treatment of beta contraction in norm_term/norm_proof, following Envir.norm_term;

minor performance tuning: more careful treatment of empty environment;

clarified signature;

more zproofs;

clarified signature: support shared cache;

tuned;

tuned: avoid shadowing;

more zproofs;

tuned;

more operations; clarified cache;

tuned signature;

tuned names;

tuned -- eliminate clones;

tuned;

more operations;

more operations;

tuned;

clarified signature;

tuned;

tuned;

consider schedule calculation time in estimation;

compare previous build schedule with new one, to prevent regressions;

clarified: build schedules may be outdated when empty, after some time, or due to build progress;

store previous build jobs in graph so schedules can be used later in the build process;

add serial for build schedule to avoid unnecessary db read/writes;

tuned;

clarified;

tuned;

use build database to synchronize build schedule computed on master node (e.g., such that view on cluster is consistent);

add build uuid to schedule;

tuned;

use schedule directly instead of extra cache;

added build schedule command-line wrapper;

added graphical representation of build schedules;

clarified build heuristics parameters;

proper parallel paths: factor in elapsed time;

performance tuning: cache estimates;

misc tuning and clarification;

tuned;

misc tuning and clarification, following Term.incr_bv / Term.incr_boundvars;

tuned;

tuned;

minor performance tuning: regular Same.operation;

clarified signature: more standard argument order;

clarified signature: more standard argument order;

tuned whitespace;

tuned: more standard names;

clarified signature;

tuned: prefer Same.commit;

tuned: more standard argument order;

clarified signature;

more operations; more caching;

tuned comments;

tuned structure;

tuned;

merged

performance tuning: cache for ztyp_of within zterm_of; clarified signature;

tuned names;

minor performance tuning;

more zproofs;

minor performance tuning;

tuned;

more zproofs;

clarified modules;

more zproofs;

more zproofs;

proper treatment of ZConstP: term represents body of closure;

proper substitution of types within term;

more accurate treatment of term variables after instantiation of type variables;

tuned signature;

tuned;

check that Isar proofs contain one 'show'

include unnamed chained facts in Sledgehammer's relevance filter

merge

removed hack in Sledgehammer that confuses preplay and gives Sledgehammer a strange semantics

don't freeze terms in Sledgehammer, as this has a bad impact on 'using' facts

tuned T functions: now 0 if not recursive

minor performance tuning;

tuned;

more zproofs; clarified signature;

misc tuning and clarification; eliminate clones (see also 3ae09d27ee7a);

more zproofs;

more operations;

more operations;

tuned;

clarified signature;

more zproofs;

more ML pretty-printing;

clarified const_proof vs. zproof_name;

merged

more zproofs; misc tuning and clarification;

tuned;

tuned;

more operations; tuned semicolons;

clarified modules; more source positions;

more zterm operations; more zproofs;

compactified specification of type class parity

generalized

explicit annotation of lemma duplicates

merged

clarified proof_body: cover zboxes from zproof;

pro-forma support for optional zproof: no proper content yet;

clarified signature: follow Term.could_unify;

clarified bootstrap --- modules related to proofterm.ML;

clarified path time heuristic: configurable parameters for larger search space;

clarified heuristics toString; add generator description to schedule;

tuned;

add heuristic for non-scheduled (standard) build behaviour;

proper unused nodes;

clarified schedule message;

proper parallel paths;

clarified build schedule host: more operations;

clarified path heuristic;

clarified graph operations in timing heuristic;

merged

added and removed [simp]s

tight representation of types / terms / proof terms (presently unused);

merged