tuned output -- avoid bombing of Scala toplevel, e.g. for AFP deps;

more direct implementation of distinct_subgoals_tac -- potentially more efficient;

tuned;

HOL-SPARK .prv files are no longer written to the file-system;

updated to postgresql-42.2.5;

merged

fix (non-existent) document generation

updated to scala-2.12.7;

news

de-emphasize HOL-SPARK: somewhat outdated;

proper naming conventions for contexts;

permissive declaration attribute "relator_mono", e.g. relevant for Binomial-Heaps.BinomialHeap with -o export_theory;

tuned spelling;

tuned whitespace and sections;

tuned -- eliminated clone;

suppress aux. locales from command 'experiment' -- avoid crash of theory Dict_Construction.Test_Dict_Construction (AFP);

obsolete (see 6f8ae6ddc26b);

updated to new list_update precedence

avoid confusing precedences

more direct locale goal: avoid renaming of type_parameters;

adapted to Library/LaTeXsugar

const_typ also works for fixed variables - useful primarily for locales

tuned message according to ML version;

more liberal: detect free-form infixes as well, e.g. Orderings.ord_class.less_eq;

more accurate syntax: e.g. avoid brackets as prefix notation;

more approximative prefix syntax, including binder;

proper syntax for locale vs. class parameters;

simpler def

tuned signature;

tuned signature;