tuned signature;

just one timing protocol function, with 3 implementations: TTY/PG, PIDE/document, build;

clarified protocol_message undefinedness;

quote by Alan Kay;

more accurate documentation;

discontinued Toplevel.no_timing complication -- also recovers timing of diagnostic commands, e.g. 'find_theorems'; print timing as tracing, to keep it out of the way in Proof General; no timing of control commands, especially relevant for Proof General;

more accurate documentation of "(structure)" mixfix;

more robust static structure reference, avoid dynamic Proof_Context.intern_skolem in Syntax_Phases.decode_term;

tuned comment;

just one syntax category "mixfix" -- check structure annotation semantically;

tuned message;

handle case clashes on Mac file system by encoding goal numbers

avoid duplicate "tcon_" names

smoothly handle cyclic graphs

compile + fixed naming convention

reverted accidental changes to theory file + updated wrt ML file

no need to filter tautologies anymore -- they are prefiltered by "all_facts"'

work on CASC LTB ISA exporter

tuning

add continuous_on rules for products

fixed spelling

move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative

remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)

improved printing of exception CTERM (see also d0f0f37ec346);

prefer pretty_exn where possible -- NB: low-level General.exnMessage may still be used elsewhere (e.g. by the ML compiler itself);

more defensive representation of forced break within PolyML.PrettyBreak -- avoid accidental blowup if low-level operations are used, notably PolyML.makestring or its variant General.exnMessage;

discontinued odd magic number, which was once used for performance measurements;

document @{make_string}, cf. NEWS of Isabelle2009-2 (June 2010);

merged

more general Thy_Load.import_name, e.g. relevant for Isabelle/eclipse -- NB: Thy_Load serves as main hub for funny overriding to adapt to provers and editors;

try to preserve original linearization

use somewhat lighter encoding

robustness w.r.t. unknown arguments

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;