more antiquotations;

misc tuning to accomodate scala-2.10.0-M2;

include scala.xml as of scala-2.9.1.final/misc/scala-tool-support/jedit/modes/scala.xml -- seems to be missing in more recent distributions;

merged

merged

tidying and structured proofs

refined Local_Theory.define vs. Local_Theory.define_internal, which allows to pass alternative name to the foundational axiom -- expecially important for 'instantiation' or 'overloading', which loose name information due to Long_Name.base_name cooking etc.; actually make "raw_def" internal (cf. 80123a220219);

tuned proofs;

simultaneous read_fields -- e.g. relevant for sort assignment;

added Syntax.read_typs; tuned parallelism for syntax operations;

renamed HOL-Matrix to HOL-Matrix_LP to avoid name clash with AFP;

tuned message;

tuned proofs;

tuned proofs;

tuned exception;

merged;

spelt out missing colemmas

generalized INF_INT_eq, SUP_UN_eq

tuned specifications

sort via string_ord (as secondary key), not fast_string_ord via Symtab.fold; tuned;

tuned grouping -- merely indicate order of magnitude;

slightly more parallel find_theorems;

'definition' no longer exports the foundational "raw_def";

some attempts to fit source on screen;

eliminated odd 'finalconsts' / Theory.add_finals;

modernized axiomatization; eliminated odd 'finalconsts';

modernized axiomatization; eliminated odd 'finalconsts';

afford strict Args.type_name (cf. 29e88714ffe4);

check declared vs. defined commands at end of session;

more abstract heading level;

less redundant data;

uniform keyword names within ML/Scala -- produce elisp names via external conversion; discontinued obsolete Keyword.thy_switch;

merged

ZF news

merged

Structured transfinite induction proofs

make more word theorems respect int/bin distinction

outer syntax command definitions based on formal command_spec derived from theory header declarations;

refute_params are given in *this* theory;

defer actual parsing of command spans and thus allow new commands to be used in the same theory where defined;

define keywords early when processing the theory header, before running the body commands;

clarified Keyword.is_keyword: union of minor and major; misc tuning and simplification;

Isabelle/jEdit supports user-defined Isar commands within the running session;

merged

beautification and structured proofs

replacing ":" by "\<in>"

Rewrote some induction proofs to be structured

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;