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;

clarified modules; more conventional GUI threading;

Merge

Dead wood removal

Merge

real_of_nat_Suc is now a simprule

updated docs

clarified Isabelle_System.init; clarified GUI.init_laf; clarified modules; tuned signature;

tuned;

tuned GUI;

proper event;

tuned GUI;

build session within running jEdit;

clarified modules;

monomorphization of divmod wrt. code generation avoids costly dictionary unpacking at runtime

more selective preprocessing allows bare "numeral" occurences to be retained as real function in generated code

Caratheodory: cleanup and modernisation

restructure fresh variable generation to make exports more wellformed

more canonical context threading

merged