more robust access to shared libraries for poly executable: avoid global change of LD_LIBRARY_PATH (e.g. relevant for subprocesses);

Merged

Some lemmas about complex sinh/cosh/tanh

more elementary proof of connected_Times, earlier

merged

tuned

Added hyperbolic functions

added lemmas, avoid 'float_of 0'

clarified signature;

more uniform treatment of formal comments within document source; more robust nesting;

just one check of formal comments;

avoid proliferation of language_document reports; clarified signature;

more external tools for AFP test;

clarified overall range: include delimiters;

added lemma

tuned: more standard use of order;

tuned;

tuned;

clarified signature; eliminated aliases of Thm.term_ord;

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;

tuned;

unused;

clarified access to antiquotation options; define explicit variants of antiquotations; output proper Latex.text; misc tuning and clarification;

more operations;

tuned signature;

discontinued unused wrapper: print_mode is provided directly;

corrected name

moved from AFP/Gromov

moved from AFP/Gromov

added lemma

moved from AFP/Gromov

moved t3/t4 space from AFP/Gromov to here.

more automation

more lemmas by Gouezele

move lemmas by Gouezel to distribution

Experimental support for rewrite morphisms in locale instances.

tuned signature;

more documentation;

clarified markup;

discontinued old form of marginal comments;

tuned document;

clarified comments;

standardized towards new-style formal comments: isabelle update_comments;

uniform treatment of old-style and new-style comments;

tuned signature;

clarified markup;

more uniform support for formal comments in outer syntax, notably \<^cancel> and \<^latex>;

clarified modules; more operations;

tuned

eliminated clones;

trim blanks -- more thoroughly than in update_cartouches (for single-line comments);

more operations (as in ML);

more specific tool "isabelle update_comments", for uniformity with formal comments in embedded languages;

clarified Token.is_text (cf. Parse.text in ML);

more operations;

support for completion;

allow LaTeX source as formal comment;

clarified signature;

clarified SML (no formal comments) vs. Isabelle/ML (arbitrary comments);

clarified signature;

clarified modules: uniform notion of formal comments;

added glyph from "Deja Vu Sans Mono" font;

tuned messages;

merged

allow TeX comment % in formal comment body, but avoid extra space (cf. d7c6054b2ab1);

tuned;

tuned;

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 {* ... *};

tuned;

clarified output: avoid extra space;

output token content with formal comments and antiquotations;

tuned;

clarified signature;

clarified modules;

inner syntax comments may be written as "\<comment> \<open>text\<close>";

spelling

corrected op

tuned op

tuned op

tuned op

tuned op

tuned op's

tuned op

tuned op

tuned op's

Renamed (^) to [^] in preparation of the move from "op X" to (X)