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

tuned (reordered) code

clean up MaSh export a bit

clean up MaSh evaluation driver

merged

tuned;

clarified quasi-generic PIDE;

misc updates for release;

more release notes;

Library/Tree: bst is preferred to be a function

Library/Tree: use datatype_new, bst is an inductive predicate

more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs

import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure

some lemmas about the indicator function; removed lemma sums_def2