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;

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;

tuned strip_alls;

allow redefining pretty/markup modes (not output due to bootstrap issues) -- to support reloading of theory src/HOL/src/Tools/Code_Generator;

some grouping of Par_List operations, to adjust granularity;

Par_List.map is already smart;

some support for grouped list operations;

merged;

merged

NEWS

use eventually_elim method

add eventually_elim method

merged

tuned proofs

tuned pred_set_conv lemmas. Skipped lemmas changing the lemmas generated by inductive_set

tuned simpset

activate_notes in parallel -- to speedup main operation of locale interpretation;

refined activate_notes: simultaneous transformation before activation; actually export all_registrations_of;

tuned headers;

merged

Structured proofs in ZF

refined define_command vs. run_command: static tokenization vs. dynamic parsing, to increase the chance that the proper transaction is run after redefining commands (NB: requires slightly more space and time for document state);

updated polyml/build option to prefer included libffi;

tuned signature;

clarified prepare_positions: always retain source positions to allow using it as formal information, not just markup reports;

merged

renewing Executable_Relation

tuned;

more direct Name_Space.defined_entry; tuned Variable.export_inst: avoid keeping full contexts within the gen_fixesT closure (NB: locale infrastructure stores morphisms persistently);

eliminated old-fashioned 'constrains' element;

modernized locale expression, with some fluctuation of arguments;