more robust File.eq, and thus File.copy of "~~/lib/logo/isabelle.gif";

fixed recursor definition for datatypes with inner products (e.g. "'a trm" from the lambda-term example)

tweaked corecursor/coiterator tactic

changed the type of the recursor for nested recursion

fixed quick-and-dirty mode

tuning

use Thm.close_derivation in theorems proved using Skip_Proof.prove; tuned signature;

got rid of subst_tac alias

tuned tactic

tuned proofs;

tuned proofs;

proper handling of constraints stemming from idtyp_ast_tr';

enable show_markup by default (approx. double output size);

more explicit Syntax_Trans.mark_bound_abs/mark_bound_body: preserve type information for show_markup;

explicit show_types takes preferenced over show_markup;

ignore wrapped markup elements in Proof General;

turn constraints into Isabelle_Markup.typing, depending on show_markup options; proper recursion in standard_format;

treat wrapped markup elements as raw markup delimiters;

tuned signature;

tuned proofs;

tuned proofs;

tuned proofs;

tuned;

support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;

merged

eliminated dead code;

smarter handling of tracing messages;

display number of tracing messages;