nbe decides equality of abstractions by extensionality

eliminated some generated comments;

merged

merged

keep type variable arguments of datatype constructors in bookkeeping

document changes in Nitpick and MESON/Metis

renamed "trace_me{son,tis}" and "verbose_metis" to have the name of the tool first

put facts found by SMT solver in alphabetical order and omit chained facts, as was done already for ATP proofs

make two copies (!) of Library.UnequalLengths coincide with ListPair.UnequalLengths;

just one version of fold_rev2;

explicit use of unprefix;

keep private things private, without comments;

eliminated some clones of eq_list;

merged

new lemma

lemma trans_sym allows single-step "normalization" in Isar, e.g. via moreover/ultimately;

prefer non-classical eliminations in Pure reasoning, notably "rule" steps;

discontinued global "Isabelle" symlink, to make each distribution even more self-contained;

more correct spelling;

globbing constant expressions use more idiomatic underscore rather than star

globbing constant expressions use more idiomatic underscore rather than star; precised

datatype constructor glob for code_reflect

merged

merged