cleaned

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;