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

merged

proper input event handling;

more standard imports;

more specific Entry painting; ignore theories with all commands below threshold;

tuned;

mixed theory/command entries; tuned;

dockable window for timing information;

no \FIXME macro for ProgProve (moved to book)

remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces

rename eventually_at / _within, to distinguish them from the lemmas in the HOL image

move theorems about compactness of real closed intervals, the intermediate value theorem, and lemmas about continuity of bijective functions from Deriv.thy to Limits.thy

Series.thy is based on Limits.thy and not Deriv.thy

move Ln.thy and Log.thy to Transcendental.thy