more precise TPTP keywords and dependencies;

declare command keywords via theory header, including strict checking outside Pure;

prefer formally checked @{keyword} parser;

added ML antiquotation @{keyword};

declare minor keywords via theory header;

more explicit header_edits before main text_edits; handle reparses caused by syntax update;

declare keywords as side-effect of header edit; parse_command span is now lazy instead of future, to happen synchronously after header edit in new_exec (before execution);

more recent recent_syntax, e.g. relevant for document rendering during startup;

clarified syntax of prospective keywords;

basic support for outer syntax keywords in theory header;

maintain Version.syntax within document state; clarified Outer_Syntax.empty vs. Outer_Syntax.init, which pulls in Isabelle_System symbol completions;

explicit Outer_Syntax.Decl;

allow multiple 'keywords' as in 'fixes'; tuned comments;

some support for outer syntax keyword declarations within theory header; more uniform Thy_Header.header as argument for begin_theory etc.;

merged

merged

structured case and induct rules

rudimentary documentation test

doc-src build option (for emerging mira configuration)

corrected fragile proof; tuned semicolons

rudimentary distribution build configuration

support for non-HTTP repository locations (important for mira); quasi-hardwired repository name

corrected slip

merged

rationalising the induction rule trans_induct3

allow modification of REPOS_NAME and REPOS from outside

locale expressions without source positions;

tuned;

tuned messages;

source positions for locale and class expressions;

some proof indentation;

more explicit indication of swing thread context;

more indentation;

prefer asynchronous context switch from actor to swing thread, to reduce danger of deadlocks; more robust use of Session.Commands_Changed vs. Document_View.visible_range as asynchronous swing task, taking into account that the model might have switched in the meantime (e.g. via fast clicking on hypersearch while the prover is crunching);

eliminated obsolete sanitize_name;

Local_Theory.define no longer hard-wires default theorem name -- targets/packages need to take care of it;

more parallel inductive_cases; more explicit indication of def names;

misc tuning;

updated to jedit_build-20120313 with jedit-4.5.0; updated version information;

tuned context specifications and proofs;

tuned proofs;

clarified command state -- markup within proper_range, excluding trailing whitespace;

more explicit indication of def names;

merged

Structured proofs concerning the square of an infinite cardinal

suppress vacous notes elements, with subtle change of semantics: 'interpret' no longer pulls-in unnamed facts "by fact";

prefer abs_def over def_raw;

prefer abs_def over def_raw;

improved attribute "abs_def" to handle object-equality as well;

merged

More structured proofs about cardinal arithmetic

tuned proofs;

refined 'interpret': reset facts ("this") and print_result, which merely consist of internal / protected statement;

tuned proofs -- eliminated pointless chaining of facts after 'interpret';

proper printing of empty binding (again, cf. 93f6f24010c2);

tuned;