global start time as reference point;

tuned signature -- clarified modules;

obsolete (see 9c6346319eee, 7924d61b50cf);

added splay trees

added many small lemmas about setsum/setprod/powr/...

no icons here -- not a standalone window;

workaround for problem with C-1, C-2, C-3 seen on Slovak QWERTY keyboard;

removed presumably obsolete workaround (see 7924d61b50cf);

Cauchy's integral formula, required lemmas, and a bit of reorganisation

merged

new lemmas about topology, etc., for Cauchy integral formula

adapted to 436b7fe89cdc

clarified Latex.environment (again, amending e16649b70107): avoid additional paragraph, e.g. relevant for option [display];

added 234-trees (slow)

added 234-Trees (slow)

tuned

more uniform command-line for "isabelle jedit" and the isabelle.Main app wrapper;

updated to jedit-5.3.0 and SideKick 1.8;

updated to jdk-8u66;

print thm wrt. local shyps (from full proof context); tuned;

clarified modules; tuned signature;

proper transfer of stored facts;

tuned;

more robust ASCII output: avoid ligatures of quotes;

tuned;

more control symbols; tuned;

clarified scan_cartouche_depth (amending 8284c0d5bf52): finish after outermost cartouche;

rendering for \<^verbatim>;

Isabelle fonts via external component;

tuned document;

tuned document;

added glyphs 0x25a9 from DejaVuSansMono;

removed generated files from repository;

tuned;

proper spaces around @{text};

isabelle update_cartouches -t;

added isabelle update_cartouches option -t;

another antiquotation short form: undecorated cartouche as alias for @{text}; document antiquotation @{text} ignores option "source";

repaired document;

more symbols; tunes whitespace;

tuned English;

more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;

tuned document;

merged

avoid odd permissions of fresh tmp_file;

added action "isabelle-emph"; changed shortcut of action "isabelle-reset";

tuned;

tuned;

tuned text

tuned;

merged

more control symbols;

tuned signature;

tuned signature;

clarified;

clarified control antiquotations: decode control symbol to get name; document antiquotations @{emph}, @{bold}; symbol interpretation for \<^emph>; tuned;

more documentation;

support control symbol antiquotations;

clarified Symbol.is_control;

added 2-3 trees (simpler and more complete than the version in ex/Tree23)

code abbreviation for mapping over a fixed range

back to lxbroy3, which appears to be free at the moment;

tuned signature;

merged

more uniform command setup;

added 'paragraph', 'subparagraph';

clarified Latex.environment;

more explicit output of list items;

tuned;

clarified nesting of paragraphs: indentation is taken into account more uniformly; tuned;

Markdown support in document text;

clarified Antiquote.antiq_reports; Thy_Output.output_text: support for markdown (inactive); eliminared Thy_Output.check_text -- uniform use of Thy_Output.output_text;

trim_blanks after read, before eval; clarified Raw_Token: uniform output_text; tuned signature;

clarified modules;

load markdown.ML into Pure;

proper recursive nesting of adjacent lists;

tuned;

clarified line content: source without marker prefix;

more markup;

report Markdown document structure;

more comments;

unused -- avoid confusion in Symbols dockable;

proper nesting of adjacent lists;

more document structure; tuned signature;

more document structure;

more document structure;

clarified;

minimal support for Markdown documents;

clarified;

more symbols;

more symbols;

clarified control symbols;

added glyphs 0x21e4, 0x21e5, 0x27a7 from DejaVuSansMono;

tuned signature (cf. XML.trim_blanks);

added split_lines; tuned signature;

qualify some names stemming from internal bootstrap constructions

removed too aggressive underscorization

typo

prefer undecorated typedef

even -> evn to avoid clash with global even

added invar empty

Fixed nonterminating "blast" proof

new material on path_component_sets, inside, outside, etc. And more default simprules

restored print translation from a1141fb798ff, to prevent a printing misfit observable using "thm divmod_nat_if" in theory "Divides", with a meagure indication in the comment

prod_case as canonical name for product type eliminator

emphasized general nature of parameter

moved lemmas

more symbols;

redundant due to \parindent 0pt;

isabelle update_cartouches;

scalable fonts for T1 encoding;

proper imports; more symbols; avoid special latex tricks;

more symbols;

more symbols;

more antiquotations;

proper message;

clarified antiquotation;

spelling;

unused;

obsolete;

@{verbatim [display]} supersedes old alltt/ttbox;

@{verbatim [display]} supersedes old alltt/ttbox;

more symbols;

some control symbols for markup and formatting;

allow control symbols within markup body;

added glyphs 0x2501, 0x2508, 0x2509, 0x25aa, 0x25b8 from DejaVuSansMono;

proper document source;

tuned syntax -- more symbols;

tuned syntax -- more symbols;

tuned syntax -- less symbols;

tuned syntax -- more symbols;

tuned syntax -- more symbols;

tuned syntax -- more symbols;

tuned syntax -- more symbols;

tuned syntax -- more symbols;

tuned syntax -- more symbols;

tuned syntax -- more symbols;

tuned syntax -- more symbols;

tuned whitespace;

tuned;

tuned syntax -- more symbols;

more symbols;

more symbols;

more symbols;

prefer symbols;

use Isabelle symbols by default;

isabelle update_cartouches;

more explicit HTML.symbols; tuned signature;

NEWS;

more direct HTML presentation, without print mode;

discontinued specific HTML syntax;

installable TTF for MS IE 9+;

output HTML text according to Isabelle/Scala Symbol.Interpretation;

tuned output;

server-side fonts;

more accurate imitation of "cp -p -f";

more Present operations on Scala side;

clarified, according to Isabelle_System.copy_file in ML;

NEWS

documentation for transfer debug methods

add a file with examples of debugging transfer

new methods for debugging transfer and transfer_prover

right parenthesization

made TPTP SZS status more compliant

tuning

measurable sets on product spaces are embeddings of countable products

generalize eqI theorems for product measures

isabelle update_cartouches;

more glyphs from DejaVuSansMono and DejaVuSansMono-Bold: 0100-017F Latin Extended-A, 0180-024F Latin Extended-B;

cleanup projective limit of probability distributions; proved Ionescu-Tulcea; used it to prove infinite prob. distribution

avoid 'legacy binding' warning

removed dead code

merged

back to old-fashioned GC, which appears to work better with interactive applications;

routine check of theory context;

proper context;

proper context;

clarify docs

updated docs

made documentation more accurate

disable generation of 'case_transfer' for 'nibble', due to quadratic proof -- to make 'HOL-Proofs' happier

avoid unsound 'nitpick_simp' attribute on nonterminating, nonproductive equations

parallel tests: 6h & 12h;

news

generate 'case_transfer' unconditionally

isabelle update_cartouches;

isabelle update_cartouches;

merged

avoid hardwired frees; tuned;

added Thm.forall_intr_name;

added 'proposition' command;

fewer aliases for toplevel theorem statements;

just one theorem kind, which is legacy anyway;

pretty_const: proper local name space; tuned;

collect the names from goals in favor of fragile exports

compile

tuning

avoid legacy syntax

further improved fine point w.r.t. replaying in the presence of chained facts and a non-empty meta-quantifier prefix + avoid printing internal names in backquotes

added "!=" (disequality) as a TPTP binary operator, since it pops up in LEO-II proofs

merged

tuned signature;

produce nodes_status outside GUI thread, to avoid a few milliseconds of blocking;

avoid too aggressive optimization of 'finite' predicate

avoid unsound simplification of (C (s x)) when s is a selector but not C's

extended theory exporter to also export MePo-selected facts

speed up MaSh duplicate check

sped up MaSh nickname generation

merged

more explicit umask for important directories: e.g. relevant for Windows 10, where implicit g=rwx leads to odd failure of chmod -w for heap images;

speed up MaSh

updated docs and NEWS

updated docs

removed Nitpick nonblocking mode, that was never really used

adapted example

removed obsolete material in documentation

further reduced dependency on legacy async thread manager

removed legacy asynchronous mode in Sledgehammer

better compliance with TPTP SZS standard

merged

avoid useless empty case_names;

clarified init (again): isabelle.Main is responsible to provide basic JVM setup, jedit.jar picks this up (e.g. list of known fonts), plugin cannot be loaded in isolation without isabelle.Main;

New theorems about connected sets. And pairwise moved to Set.thy.

less ambitious regex -- avoid unclarities of escaping;

tuned documentation

tuned datatype docs

export proof method in signature

export '_cmd' functions

back to old JavaAppLauncher to avoid initial startup problems (due to unsigned application?);

tuned GUI;

proper isabelle.root for bootstrap;

merged

tuned;

proper Cygwin.init (amending e00e1bf23d03);

renamed jvmpath to platform_path;

clarified ISABELLE_ROOT (platform path) vs. ISABELLE_HOME (standard path);

tuned GUI;

uniform treatment of bootstrap directories; Isabelle_System.init() includes Cygwin.init(), e.g. for situations without isabelle.Main; tuned;

more robust system init (again), in case the plugin is started without isabelle.Main;

tuned message;