do not conceal inductive predicate names properly, following 4a3747517552

tuned

renamed "pairself" to "apply2", in accordance to @{apply 2};

added ML antiquotation @{apply n} or @{apply n(k)};

even more exception traces for Document.update, which goes through additional execution wrappers;

more informative failure of protocol commands, with exception trace; eliminated obsolete Runtime.TERMINATE (left-over from former 'exit' command);

load simple_thread.ML later, such that it benefits from redefined print_exception_trace;

tuned proof that pmfs are bnfs

projections of pair_pmf (by D. Traytel)

merged

removed odd remains of structural containment checks, which stem from an older approach (see also 3ad1b289f21b, 3ae3cc4b1eac, 423af2e013b8, bad13b32c0f3, ccd6de95f4a6); de-facto this alternative never occured in practice, but it can lead to non-termination of the check;

preinstantiate (co)inductions in N2M to handle mutual but separated SCCs

add congruence solver to measurability prover

cleanup measurability prover

updated SMT certificates

added one more CVC4 option that helps Judgment Day (10 theory version)

tuned whitespace

keep all 'ctr' theorems

smoothly handle unit codatatypes in 'primcorec'

careful with de Bruijn indices

improved message in 'co' case

updated NEWS

no need for subset operation as a primitive in Nitpick, esp. that its implementation was unsound (cf. Rene Thiemann's 16 Oct 2014 email on isabelle mailing list)

added Z3 reconstruction rule suggested by F. Maric

one more CVC4 option that helps

renamed 'veriT' to 'verit', to stick to all-lowercase rule for prover names

update CVC4 version docs

tuned signature;

tuned;

misc tuning and modernization;

misc tuning and modernization;

more careful ML source positions, for improved PIDE markup;

named_theorems: multiple args;

tuned;

removed some add-ons from modules that are relevant for the inference kernel;

add lemma following a proof suggestion by Joachim Breitner

add lemma

register pmf as BNF

added CVC4 option that helps on JD

always generate patterns as lists of lists, to avoid confusing CVC4 (and stick to what SMT-LIB 2 actually says)

work around bug in CVC4, with boolean arguments to (co)datatypes

other way of crashing (with CVC4)

set right logic for CVC4 with (co)datatypes

removed explicit '--quant-cf' option to CVC4, now that it's the default

more accurate lemma name

parse CVC4 unsat cores

tuning

removed redundant code line

clarified Table.make_set: duplicate arguments are allowed, like Table.make_list or Scala Set() formation;

add reindex rules for distr and nn_integral on count_space

generalized lemmas and tuned proofs

generalized lemmas (particularly concerning dvd) as far as appropriate

formally self-contained gcd type classes

merged

no quick_and_dirty for proof extraction, to avoid obscure errors like "corr: bad proof";

use \isastyletext directly via 'text' command;

proper sequential version (cf. 302104d8366b);

documentation stubs about permanent_interpretation

cleaning up some theorem names; remove unnecessary assumptions; more complete pmf theory

merged