added certify_inst, certify_instantiate;

merged

trans_tac: use theory from goal state, not the static context, which seems to be outdated under certain circumstances (why?);

proper Jinja-Slicing;

merged

merged

abstractions: desymbolize name hint

added numeral code postprocessor rules on type int

sos comments modified

sos documentation

Added remote-SOS changes by Philipp Meyer

Functionality for sum of squares to call a remote csdp prover

merged

updated generated document

reinserted legacy ML function

Set.UNIV and Set.empty are mere abbreviations for top and bot

explicit is better than implicit

Meson.first_order_resolve: avoid handle _; proper context for various Meson and Metis rules and tactics unified meson_tac/meson_claset_tac;

removed old global get_claset/map_claset; added local get_claset/put_claset;

eliminated METAHYPS;

Future.shutdown before loading sequentially -- workaround scheduler deadlock;

ResAxioms.neg_conjecture_clauses: proper context; let exceptions get through unhindered -- Poly/ML exception_trace will do the tracing;

neg_conjecture_clauses, neg_clausify_tac: proper context, eliminated METAHYPS; external_prover: neg_conjecture_clauses should handle TVars within goals; misc tuning;

Hilbert_Classical: sequential loading due to @{prf}, which joins within a critical section (via options);

eliminated separate Future.enabled -- let Future.join fail explicitly in critical section, instead of entering sequential mode silently;

non-critical use_thy;

future result: Synchronized.var;

added unsynchronized Synchronized.peek;

group status: Synchronized.var;

tuned;