bold version: math glyphs from plain IsabelleMono;

fixed rangle;

use dash from text font, not math;

added glyphs for \<A> (cal), \<a> (rm), \<AA> (\frak), \<aa> (frak); replaced old-style digits by bold ones (bf);

generated ttf;

renamed to IsabelleMono;

added README with original licenses;

renamed Isabelle to IsabelleItalic;

fixed rangle glyph;

the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;

Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);

Isabelle font, based on TeX glyhps;

enable future_scheduler by default;

ISABELLE_USEDIR_OPTIONS: -M max is default;

unified ids for ancestors and checkpoints, removed obsolete history of checkpoints; tuned representation of internal node names -- avoid string copies; tuned signature;

removed spurious exception_trace;

print_theorems: more robust difference, even after finished proof;

export context_node;

merged

more antiquotations;

pcpodef package: state two goals, instead of encoded conjunction;

recovered goal_pat;

inhabitance goal is now stated in original form and result contracted -- the previous attempt with contracted goal and initial unfolding did not work, because it disrupted the Isar proof structure (e.g. ?thesis);

tuned signature: pcpodef_proof, pcpodef_proof_cmd etc.; more antiquotations; explicit Theory.requires; adapted to recent changes in ~~/src/HOL/Tools/typedef_package.ML; misc tuning and simplification;

add_typedef: unfold set_def in tactical proof as well;

merged

Theory.checkpoint before commencing proof;

misc tuning and modernisation;