cleaned

tuned

tuned signature -- agree with markup terminology;

unified terminology with Markup.DOCUMENT_SOURCE in Scala, which is unused but displayed as "document source" entity in Isabelle/jEdit;

tuned document

tuned

sup on multisets

convenient induction rule

tuned README -- less buzzwords;

more conventional synchronized access to Options_Variable -- avoid Swing_Thread getting in the way, which might be absent in some environments (e.g. SWT);

added missing file;

tuned signature -- avoid intrusion of slightly odd Swing structures into pure Markup_Tree;

tuned signature -- concentrate GUI tools;

tuned signature -- concentrate GUI tools;

separate module "GUI", to keep this out of the way of generic Isabelle_System operations, notably for non-Isabelle/jEdit applications; tuned signature;

separate module Isabelle_Font, to keep this out of the way of generic Isabelle_System operations, notably for non-Isabelle/jEdit applications;

tuned imports;

added var_position in analogy to longid_position, for typing reports on input; avoid duplicate token var report;

removed unnerving (esp in jedit) and pointless warning

tuned

merged

tuned;

recover implicit thread position for status messages (cf. eca8acb42e4a);

additional timing status for implicitly forked terminal proofs -- proper accounting for interactive Timing dockable etc.;

more explicit Goal.fork_params -- avoid implicit arguments via thread data; actually fork terminal proofs in interactive mode (amending 8707df0b0255);

updated comment to 46b90bbc370d;

recovered proper transaction position for Goal.fork error reporting (lost in 8e9746e584c9);

tuned -- Drule.comp_no_flatten includes Drule.incr_indexes already (NB: result should be deterministic by construction);

tuned output -- less bullets;

default implementation of multisets by list with reasonable coverage of operations on multisets

optionalized very specific code setup for multisets

generalized lemma fold_image thanks to Peter Lammich

tuned;

NEWS for 635562bc14ef;

more centralized command timing; clarified old-style timing message;

got rid of legacy smartness

added lemma

merged

amended uncond_skel to observe notion of cong_name properly -- may affect simplification with Free congs;

more formal cong_name;

timing status for forked diagnostic commands;

tooltip of command keyword includes timing information;

more operations on Time, Timing;

reverted slip introduced in f738e6dbd844

added 'print_defn_rules' command; tuned;

more item markup; tuned signature;

item markup for Proof_Context.pretty_fact; tuned signature;

obsolete, cf. Proof_Context.print_syntax;

paint bullet bar within text layer -- thus it remains visible with active selection etc.;

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;