Pretty.item markup for improved readability of lists of items;

tuned message;

convenience check for vain instantiation

improved centering via strikethrough offset;

re-generated SMT certificates

new, simpler implementation of monomorphization; old monomorphization code is still available as Legacy_Monomorphization; modified SMT integration to use the new monomorphization code

ghost bullet via markup, which is painted as bar under text (normally space);

replace induction by hammer

merged

merged;

basic support for Pretty.item, which is considered as logical markup and interpreted in Isabelle/Scala, but ignored elsewhere (TTY, latex etc.);

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

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

move SEQ.thy and Lim.thy to Limits.thy

HOL-NSA should only import Complex_Main

rename RealVector.thy to Real_Vector_Spaces.thy

rename RealDef to Real

remove Real.thy

merge RComplete into RealDef

move real_isLub_unique to isLub_unique in Lubs; real_sum_of_halves to RealDef; abs_diff_less_iff to Rings

remove posreal_complete

separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef

Discontinued theories src/HOL/Algebra/abstract and .../poly.

Remove obsolete URLs in documentation of HOL-Algebra.

Fix issue related to mixins in roundup. Previously, mixins were only applied one level down the DFS tree while they should also be applied at the level of declaration. Makes the algorithm consistent with the version presented in the upcoming JAR paper.

simp_const -> afold; bfold -> fold'; bsimp_const -> bfold

added lemmas

merged

clarified text_fold vs. fbrk;

tuned print_classes: more standard order, markup, formatting; uniform printing of minimal supersort/classrel;

tuned message;

actually exit on scalac failure;

tuned signature;

removed obsolete uses of ext

prefer preset = 3 -- much faster and less memory requirement;

basic support for xz files;

added component xz-java-1.2;

more "quick start" hints; more explicit "Testing of changes", instead of convoluted "Building a repository version of Isabelle"; tuned;

simple case syntax for stream (stolen from AFP/Coinductive)

prefer plain \<^sub> for better rendering (both in Isabelle/jEdit and LaTeX); tuned proofs;

merged

reverted most of 5944b20c41bf -- tends to cause race condition of synchronous vs. asynchronous version;

no censorship of "view.fracFontMetrics", although it often degrades rendering quality;

retain original tooltip range, to avoid repeated window popup when the mouse is moved over the same content;

apply small result immediately, to avoid visible delay of text update after window move;

structural equality for Command.Results; more general Command.State.eq_content;

allow fractional pretty margin -- avoid premature rounding;

more explicit Pretty.Metric, with clear distinction of unit (space width) vs. average char width (for visual adjustments) -- NB: Pretty formatting works via full space characters (despite a981a5c8a505 and 70f7483df9cb); separate JEdit_Lib.pretty_metric, with slightly closer imitation of jEdit;

tuned;

spelling

fundamental revision of big operators on sets

tuned proof

locales for abstract orders

merged

added rudimentary induction rule for partial_function (heap)