tuned;

tuned;

avoid former verbose_latex, which has been renamed to verbose in 52030acb19ac;

compose Latex text as XML, output exported YXML in Isabelle/Scala;

more direct index_entry: no positions required -- text is eventually moved to .ind file;

clarified signature;

clarified system_log: make this work independently of the particular "isabelle build" command-line (e.g. "isabelle mirabelle");

tuned message, e.g. for Pure bootstrap;

proper signature export (amending b50f8cc8c08e);

syslog option for "isabelle build";

further "unset CDPATH", whenever a new non-interactive bash is started (see also ac07f6be27ea);

merged

NEWS;

clarified index, more like formal @{element_ref};

clarified treatment of type constructors;

misc tuning and clarification;

tuned signature;

clarified context;

more uniform document antiquotations for ML: consolidate former setup for manuals;

clarified names;

clarified index antiquotation for ML: more ambitious type-setting, more accurate syntax;

clarified modules;

clarified modules;

tuned;

clarified signature: avoid dispatch via name;

clarified, e.g. type variables;

tuned index;

more ambitious default for index "is like";