clarified signature: prefer proper order operation;

tuned signature: more operations;

clarified signature;

proper term_ord as in HOL/Library/positivstellensatz.ML, e.g. relevant for "0 <= c & 0 <= a ==> a + bb = 1 & c <= 1 ==> bb * c * 4 <= (12::real)";

performance fine-tuning of hot spot;

tuned;

more efficient tokens_match_ord based on token_kind_index; tuned;

more abstract type;

tuned;

clarified signature;

clarified signature;

explicit dummy token;

clarified modules;

clarified signature;

clarified breakgain: keeping it constant avoids margin fluctuation in Pretty_Tooltip vs. Pretty_Text_Area;

clarified lines: like split_lines;

tuned;

unused;

tuned;

simplified: prod_count is always NONE;

tuned;

tuned data structure and operations;

tuned data structure and operations;

tuned data structure and operations;

more operations;

prefer specific tokens_subtract: subtle change of comparison via tokens_match;

tuned type: absorb NONE: token option as token_none: token;

tuned;

clarified types and operations: potentially more efficient add_prods; tuned data structure;

clarified modules; tuned;

tuned: more explicit types;

tuned data structure: potentially more efficient add_prods;

clarified operations;

merged

expand definitions of \DeclareOldFontCommand in traditional article.cls, e.g. KOMA-Script no longer provides these;

irrelevant reference to doubtful theory Code_Char

avoid concrete (anti)mono in theorem names since it could be the other way round

more uniform documentation;

proper fall-back rendering of control symbol;

clarified take/drop/chop prefix/suffix;

clarified signature;

proper signature (amending c4e9e0c50487);

tuned output;

tuned;

explicit graph for chains, which contains all nts as nodes;

tuned;

tuned;

prefer lazy update;

tuned output;

more operations;

include lemmas generally useful for combinatorial proofs

redundant;

allow cartouche within ML string;

verbatim output consists of plain lines;

old-style inner comments are legacy;

more markup: disable spell-checker for raw latex;

clarified signature: items with \isasep are special;

clarified signature;

tuned message;

clarified operations;

tuned signature: removed unused operations;

tuned: prefer list operations over Source.source; approximative parsing of theory header;

tuned: prefer list operations over Source.source;

tuned: prefer list operations over Source.source;

clarified signature;

clarified position;

clarified operations;

merged

treat sessions as entities with defining position; tuned signature;

options file for x86_64 only (amending 03a96b8c7c06);

updated to jdk-8u162;

more robust java.ext.dirs: avoid picking up accidental jars from system directories;

drop redundant cong rules

merged

drop redundant fundef_cong rule

tuned

repair malformed fundef_cong rule

removed duplicate

tuned message: same error may occur in different contexts;

detect more errors;

merged

made sorted fun again

imported patch sorted

add lemma on lists from Falling_Factorial_Sum entry

merged

avoid evaluation of embedded comment;

disable "display" style in marginal (line) comment;

more uniform output of source / text / theory_text, with handling of formal comments etc.;

sort completion result;

recovered antiquotation check without latex mode (cf. dfc93f2b01ea);

formal treatment of documentation names;

support for completion;

adapted to a5ca98950a91;

tuned output of plain name;

clarified signature;

tuned;