merged

tuned name

new simplifier trace_op for tracing simproc calls

merged

Some new material about Ramsey's theorem, also sharpening the proof to deliver the Erdős–Szekeres upper bound on Ramsey numbers

support Zipperposition's skolemization in generated Isar proofs

improved output in simps_case_conv;

improved output in inductive module;

simplifier: no trace info from simprocs unless simp_debug = true.

deal with new-style Vampire skolemization in reconstructed Isar proofs

database performance tuning: prefer light-weight IPC over heavy-duty transactions;

tuned signature; tuned output;

tuned signature: follow PostgreSQL syntax instead of JDBC API;

more robust shutdown: interruptible database connection;

clarified signature: more convenient send/receive operations;

clarified versions for documentation;

merged

clarified signature: avoid hardwired values;

clarified IPC via database server: receive notifications quasi-spontaneously via auxiliary thread;

minor performance tuning: just 1 transaction for slices <= 1;

tuned;

tuned whitespace;

tuned signature;

clarified signature: fewer warnings in IntelliJ IDEA;

removed unused database_server (amending 32ca3d1283de);

timing function generation bug fix by Jonas Stahl

tuned signature: more types, fewer warnings in IntelliJ IDEA;

new less ad hoc implementation of the 'moura' tactic for skolemization

more thorough Store.clean_output (amending 1fa1b32b0379);

clarified signature: Build_Process tells how to clean sessions;

clarified signature;

tuned;

tuned;

minor performance tuning;

tuned;

tuned signature;

tuned, following 7a1153c95bf9;

merged

tuned signature: fewer warnings in IntelliJ IDEA;

proper usage;

recover "build_database_server" from 1fa1b32b0379: still required, e.g. in build_benchmark;

clarified signature;

more robust: make double-sure that heap digest is present;

tuned;

minor performance tuning: just one transaction for log_db without heap;

tuned;

proper store.cache.compress;

tuned whitespace;

clarified store_session: heap requires process_result.ok, but log_db is always stored; clarified ML_Heap.clean_entry vs. ML_Heap.init_entry;

unused;

tuned;

tuned names;

tuned names;

clarified database layout;

tuned signature; tuned messages;

clarified signature;

more accurate types;

build local log_db, with store/restore via optional database server; tuned messages;

propagate property "isabelle.debug", notably for Java/Scala exception trace;

tuned;