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

generalized ML function

added '_legacy' suffixes

generalized ML interface

tuning

refined experimental option of Sledgehammer

tuned;

explicit print_depth for the sake of Spec_Check.determine_type;

obsolete -- done in Isabelle_Process.init_options;

clarified use of options;

tuned signature;

clarified use of options;

avoid hardwired values;

eliminated duplicate;

more operations;

merged

merged

added Leftist_Heap

updated to scala-2.11.8;

proper SHA1 digest as annex to heap file: Poly/ML reads precise segment length;

more operations;

tuned signature;

HOL-Word: add stronger bl_to_bin_lt2p_drop

proper sectioning

sorted out type issue with sort constraints

tuned whitespace

compile

added 'corec' examples and tests

file header

added two 'corec' examples