prefer Context_Position where a context is available; prefer explicit Context_Position.is_visible -- avoid redundant message composition; tuned signature;

unused;

more uniform Execution.fork vs. Execution.print; asynchronous Execution.fork_prints, entrusted to Execution.fork management (NB: Command.print_finished is only relevant for persistent print functions);

added Execution.print: accumulate print operations for some command execution, which are applied later and print time; misc tuning;

tuned proofs

Some useful lemmas

tuned comments;

tuned load order;

superseded by (provide_)parse_files;

tuned;

merged

more warnings for recent versions of Poly/ML (see also fe1f6a1707f7);

eliminated dead code;

proper configuration option "ML_print_depth"; proper ML_exception_trace for HOL-TPTP;

removed junk;

clarified options ML_source_trace and ML_exception_trace (NB: the latter needs to be a system option, since the context is sometimes not available, e.g. for 'theory' command);

separate tokenization and language context for SML: no symbols, no antiquotes;

separate "sml" mode, suppress old "ml" mode altogether;

some SML examples;

added command 'SML_file' for Standard ML without Isabelle/ML add-ons;

updated to scala-2.10.4;

cleanup auxiliary proofs for Brouwer fixpoint theorem (removes ~2400 lines)

prove theorems with fixed variables (export afterwards)

generalized theorems about derivatives of limits of sequences of funtions

removed unused 'ax_specification', to give 'specification' a chance to become localized; tuned whitespace;

merged;

merged

proper Sign.full_name to get internal name (like Sign.add_consts);

formal check of user input, avoiding direct references of interal names;

discontinued Toplevel.debug in favour of system option "exception_trace";

tuned proofs

made tactic more robust

inline helper function

rearranging some deriv theorems

modernized approximation, avoiding bad name binding;

more sensible treatment of quasi-local variables (NB: Variable.add_fixes is only for term variables, while Variable.declare takes care of types within given terms);

merged

more antiquotations;

more antiquotations;

more antiquotations; clarified file location;

more antiquotations;

more antiquotations;

more antiquotations;

tuned message;

more antiquotations;

avoid hard-wired theory names;

generalized and strengthened cong rules on compound operators, similar to 1ed737a98198

added splash screen for jvm boot, which is important for initial encounter to avoid multiple copies running against each other;

merged

more qualified names;

more qualified names;

more qualified names;

tuned;

more qualified names;

tuned signature;

tuned signature;

a few new lemmas and generalisations of old ones

simplified internal datatype construction

merged

merged

produce qualified names more directly;

more symbols;

more static checking of proof methods;

enforce subgoal boundaries via SUBGOAL/SUBGOAL_CASES -- clean tactical failure if out-of-range;

more standard method_setup; enforce subgoal boundaries via SUBGOAL -- clean tactical failure if out-of-range;

tuned error, according to "use" in General/secure.ML;

tuned proofs;

generalize more theorems

generalize some theorems

fixing messy proofs

pointer to the other proof direction

generalize theory of operator norms to work with class real_normed_vector

tuned -- no need for slightly obscure "local" prefix;

accomodate word as part of schematic variable name;

more explicit Long_Name operations (NB: analyzing qualifiers is inherently fragile);

tuned proofs;

elongated INFI and SUPR, to reduced risk of confusing theorems names in the future while still being consistent with INTER and UNION

Some rationalisation of basic lemmas

Merge

New complex analysis material

NEWS

further renaming in Series

consolidated theorem names containing INFI and SUPR: have INF and SUP instead uniformly

merged;

clarified module arrangement;

simplified (despite 70898d016538);

clarifed module name;

tuned proofs;

clarified module arrangement; more antiquotations;

clarified modules; more antiquotations for antiquotations;

more antiquotations;

clarified bootstrap process: switch to ML with context and antiquotations earlier;

more markup for improper elements;

tuned signature;

unused;

tuned signature -- rearranged modules;

tuned proofs;

back to KeyEventInterceptor (see 423e29f1f304), but without focus change, which helps to avoid loosing key events due to quick opening and closing of popups; discontinued obsolete option jedit_completion_dismiss_delay (see 750561986828); more explicit shutdown;

remove unnecessary finiteness assumptions from lemmas about setsum

adapt to Isabelle/c726ecfb22b6

fix HOL-NSA; move lemmas

cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}

changed policy when to define constants

tuned proofs; removed duplicated facts

additional lemmas

removed dependencies on theory Ordered_Euclidean_Space

use cbox to relax class constraints

merged

tuned;

more antiquotations;

more robust machine-generated ML sources: constructors for typ and term sometimes occur elsewhere;

remove sums_seq, it is not used

update syntax of has_*derivative to infix 50; fixed proofs

unify syntax for has_derivative and differentiable

tuned proofs

tuned internal construction

a few new theorems

proper flags for main action (amending 638b29331549);

tuned rendering -- avoid flashing background of aux. files that are disconnected from the document model;

merge semantic and syntax completion; tuned;