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';