modernized definitions;

misc tuning and clarification;

check 'case' variable bindings as for 'fix', which means internal names are rejected as usual;

optional exit hook for theory-like targets

restore exactly named target, prevent non-named targets to participate in the ad-hoc switch game

centralized (ad-hoc) switching of targets in named_target.ML

add lemmas: polynomial div/mod distribute over addition

reverted 9512b867259c -- appears to break 'metis'

clarified "axiomatization" -- minor rewording of this delicate concept;

tuned;

more on ML options; suppress somewhat old Pretty.margin_default;

redundant error position, to ensure the message is attached somewhere, despite the distortion of positions due to glued tokens;

overdue NEWS concerning c4daa97ac57a

Merge

for new release

merge

document property 'rel_induct'

generate 'rel_induct' theorem for datatypes

fixed soundness bug in monotonicity-based type encodings -- the helper facts must be considered too

added hidden check to Sledgehammer fact filters, to avoid picking up facts like 'Nat.nat_induct0'

whitespace tuning

robustness in the face of ill-typed "unchecked" terms (e.g. case expressions)

use context instead of theory

fine-tuned methods

tuned message

updated docs

changed default MaSh engine

removed needless code

speed up MaSh a bit

mix NB and kNN