removed dead params and dead code

changed type of corecursor for the nested recursion case

made (co)rec tactic more robust when the simplifier succeeds early

tuned;

removed unused module Blob;

more direct message header: eliminated historic encoding via single letter;

tuned whitespace;

tuned proofs;

report sort assignment of visible type variables;

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;