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;

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