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;

simplified span class in conformance to Scala version;

discontinued specific entity markup, which causes confusion with "kind" names with spaces (e.g. "type name"); uniform treatment of "class" entities in input and output;

merged

adding tags to quickcheck's result

clarified idents for activated locales, with subtle change of semantics: insert/merge wrt. term equality, but avoid redundant_ident on retrieval; avoid confusing quasiorder ident_le as "eq" for member/merge;

eliminated dead code;