more general error suffixes, e.g. for messages that are broken over several lines;

another Latex error seen in the wild: Undefined control sequence. \isamarkupcancel #1->\xout

clarified default;

clarified formal comments;

prefer formal comments;

added \<^cancel> operator for unused text;

tuned;

restored naming of lemmas after corresponding constants

prefer formal comments;

prefer formal text;

prefer formal comments;

prefer formal comments;

isabelle update_cartouches -c;

uniform use of Standard ML op-infix -- eliminated warnings;

proper infix;

line break before op was intentional

typo

tuned notation

tuned

ran isabelle update_op on all sources

Manual updates towards conversion of "op" syntax

tuned op

tuned op's

more accurate spell-checking for nested quotations / antiquotations, notably in formal comments;

uniform typesetting of \isamarkupcmt and \isasymcomment;

more accurate position for enclosing cartouche;

tuned;

clarified signature;

clarified presentation_state with provide presentation_context;

show only symbols with code;

clarified markup: more like outer syntax side-comment;

clarified rail token language: white space and formal comments;

clarified modules;

removed duplicate text;

clarified exception;

merged;

updated to 146757999c8d;

theory Pure is default presentation context;

clarified implicit Pure.thy;

prefer qualified names;

tuned;

check formal comments recursively, within arbitrary cartouches (unknown sublanguages);

more operations;

tuned;

clarified output (see also 909dcdec2122, 34d1913f0b20);

more operations;

tuned;

moved in some material from Euler-MacLaurin

merged

prefer formal comments;

clarified NEWS;

tuned whitespace;

tuned;

support for formal comments in ML in Isabelle/Scala;

tuned;

tuned message;

allow formal comments in ML; ML_Compiler.eval: always suppress comments;

clarified modules;

tuned;

more uniform output: formal comments within {* ... *};