added reference from NEWS to docs

merged

renamed ISABELLE_BUILD_JAVA_OPTIONS to ISABELLE_TOOL_JAVA_OPTIONS;

clarified SML name space: no access to structure PolyML;

prefer internal tool;

isabelle update_cartouches -c -t;

prefer internal tool;

prefer internal tool -- assuming that ISABELLE_TMP_PREFIX is created properly by Isabelle_System.isabelle_tmp_prefix;

prefer internal tool;

prefer internal tool;

prefer internal tool;

prefer internal tool;

support for internal tools;

clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;

clarified usage;

tuned names

prefer infix operations;

structure PolyML is sealed after bootstrap: all ML system access is managed by Isabelle;

proper signature;

tuned signature;

tuned;

tuned signature;

proper type; tuned;

careful export of type-dependent functions, without losing their special status;

clarified modules;

clarified modules;

tuned LaTeX

import package that might help on some machines (e.g., macbroy2)

clarified check_sources;

obsolete (see 1d977436c1bf);

more robust display of bidirectional Unicode text: enforce left-to-right;

merged

merged

explicit warning about bidi uncertainty in Unicode;

explicit warning about formal use of Unicode;

documentation;

more markup;

require actual space;

tuned signature;

required space is already part of Position.here;

tuned messages;

clarified errors -- disallow cartouche fragments as delimiter;

tuned signature;

tuned;

clarified end position;

tuned signature;

tuned;

removed redundant Position.set_range -- already done in Position.range;

lower threshold -- command timing for proofs is cumulative, e.g. HOL 672 ~> 8889;

less bulky timing information, e.g. HOL 56913 ~> 672;

tuned;

more operations (cf. Scala version);

tuned whitespace;

explicit property for unbreakable block;

unused;

tuned markup;

clarified treatment of properties; tuned messages;

more robust pretty printing: permissive treatment of bad values;

adapted to Poly/ML repository version 2e40cadc975a;

explicit mixfix block properties;

clarified modules;

tuned signature;

reintroduced check that may guard some tactic failures

adapt theory names within the theory

made tactic more robust

tuned interface

merged

proper object-logic constraint (amending dd2914250ca7);

reconcile object-logic constraint vs. mixfix constraint;

more explicit support for object-logic constraint;

more language markup;

more accurate mixfix type constraints;

tuned;

tuned message;

more explicit type; tuned;

relevant check_mixfix happens further at the bottom, to avoid duplicate reports via Specification.prepare;

avoid duplicate reports;

tuned messages -- position is usually missing here;

more PIDE markup; tuned;

clarified modules;

clarified errors: more positions;

clarified simple mixfix;

tuned;

more operations;

updated dependencies;

updated to Navigator 2.6;

more 'corec' docs

merged

proper session dirs for "isabelle jedit" and "isabelle console" with options -d and -l;

tuned messages -- more positions;

more position information for type mixfix;

tuned signature;

proper norm_props, e.g. relevant for ML pp;

clarified reports; tuned signature;

tuned signature;

more 'corec' docs

tuning

more 'corec' docs

try tactics in right order w.r.t. schematics

more natural order for 'cong_intros'

more 'corec' documentation

renamed generated theorem

tuning

added sketchy 'corec' documentation

compile

updated Sledgehammer documentation

a more generous hard timeout

early warning when Sledgehammer finds a proof

another 'corec' example

don't ask too much of 'transfer_prover'

commented out for now

tuning

FIXME

avoid 'prove_sorry' for unreliable tactics

reused code

tuning

tuned examples

new 'corec' example

more reliable check for rhs variables

strengthened tactic