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

reduce redundancy: avoid huge lists;

more detailed profiling including "names"; avoid overlapping results;

tuned;

misc tuning and clarification;

slightly more compact heap: better sharing of persistent tuples;

added method to generate build schedules directly;

clarified load vs. apply vs. make;

tuned;

tuned heuristic;

use cpu time for approximation;

lower bound for approximated times;

use full timing information in build schedule;

consistent hosts ordering;

filter hosts properly;

merged

more compact representation of theory_id -- via consecutive thread-local ids;

misc tuning and clarification;

more compact representation;

more compact representation;

tuned signature;

more compact representation of theory_id;

tuned signature;

compact representation of sets of integers;

generated build schedule explicitly (e.g., for further analysis);

de-duplicated specification of class ring_bit_operations

generalized

restructured

grouped lemmas for symbolic computations

sorted out lemma duplicates

more reactive headless server, in contrast to 15656ad28691 (when "isabelle dump" was important to export AFP content);

tuned whitespace;

clarified signature;

clarified modules;

clarified modules; clarified transactions;

clarified modules: Build_Log.private_data provides raw data access without transaction_lock;

more thorough transaction_lock;

obsolete, see also a5896fe040dd;

removed obsolete/broken isabelle_scala_script wrapper (see also abf9fcfa65cf);

provide src/Tools/Demo as example for system component with Isabelle/Scala tool;

merged

more uniform buffer_size (see also c83cdd300848 and 26c790a6ce43);

clarified buffer_size;

merged

disable unix_domain for now: somewhat unstable, e.g. "isabelle build -b HOL-Analysis" on arm64_32-darwin (studio1);

workaround for "fix" JDK-4512626 in Java 20/21: avoid spurious caret in read-only text;

tuned;

prefer Unix-domain socket on Unix;

support for Unix-domain sockets, using java.nio.channels.ServerSocketChannel;

tuned;

clarified signature: more general make_streams;

tuned;

more robust exception handling (amending 8cc1ae43e12e);

clarified signature: avoid deprecated URL constructors;

avoid deprecated URL constructors;

proper split;

properly sort entries;

tuned;

tuned;

better estimation for unknown jobs;

clarified and tuned timing estimation;

split actual approximation from data handling;

clarified timing data vs. timing entries: full top-level data view vs. dynamic partial data;

proper filter for approximations;

proper inflection point check;

tuned;

slightly more elementary characterization of unset_bit

more direct characterization of binary bit operations

tuned;

clarified timing data operations: proper estimation (instead of known points);

use proper max threads (limited by available hardware) in heuristics;

clarified time estimation: does not use config;

handle inflection point in interpolation with monotone prefix;

proper computation of sorted prefix;

better build time interpolation: model with Amdahl's law where applicable;

proper piecewise linear build time interpolation;

properly incorporate running tasks into timing heuristic;

clarified ready vs. next ready;