removed Ids;

merged

merged

merged

Unified syntax of nominal_primrec with the one used by fun(ction) and new version of primrec command.

Modified nominal_primrec to make it work with local theories, unified syntax with the one used by fun(ction) and new version of primrec command.

merged

tuned comments; tuned;

tuned ML_OPTIONS for improved multicore performance;

refined identity and ancestry: explicit draft flat, ids are unnamed, name consistency is checked for ancestry; tuned history: renamed version to stage, disallow checkpoint/finish_thy on finished theories; added display_names -- user-level presentation; removed obsolete exists_name, names_of; tuned;

requires: check ancestors directly;

Context.display_names;

global_qed: refrain from ProofContext.auto_bind_facts, to avoid polluting the final result context with bindings involving loose free variables;

usage: echo ML settings as well;

future proofs: more robust check via Future.enabled;

removed former Isabelle font (cf. IsabelleItalic);

incorporated isabelle-fonts side-branch (forced merge);

replaced single quote by mathematical prime;

generated file;

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;