maintain integer indentation during formatting -- it needs to be implemented by repeated spaces eventually; always round block indentation upwards, to ensure that text moves visually to the right of the "hanging" part;

tuned;

proper default browser info for interactive mode, notably thy_deps;

improved pretty printing for state set acom

Improvements to the print_dependencies command.

discontinued obsolete parallel_proofs_reuse_timing;

merged

separate isatest with skip_proofs, to give some impression of performance without most of the proofs;

merged

extra checkpoint to avoid stale theory in skip_proof context, e.g. in 'instance' proof;

tuned;

allow build with skip_proofs enabled -- disable it for sessions that would fail due to embedded diagnostic commands, for example;

more robust access Toplevel.proof_of -- prefer warning via Toplevel.unknown_proof over hard crash (notably for skipped proofs);

more liberal handling of skipped proofs;

explicit Toplevel.is_skipped_proof; tuned;

separate option editor_skip_proofs, to avoid accidental change of preferences for skip_proofs, which would invalidate batch builds;

more ambitious Goal.skip_proofs: covers Goal.prove forms as well, and do not insist in quick_and_dirty (for the sake of Isabelle/jEdit);

clarified Skip_Proof.cheat_tac: more standard tactic; clarified Method.cheating: check quick_and_dirty when it is actually applied;

tuned signature and module arrangement;

tuned;

tuned GUI;

centralized various multiset operations in theory multiset; more conversions between multisets and lists respectively

avoid odd foundational terms after interpretation; more uniform code setup

more uniform style for interpretation and sublocale declarations

merged

tuned session specification;

tuned proof;

tuned imports;

tuned proofs;

explicit sublocale dependency for Min/Max yields more appropriate Min/Max prefix for a couple of facts