more neg_clausify proofs that get replaced by direct proofs

redo some of the metis proofs

back to Vampire 9 -- Vampire 11 sometimes outputs really weird proofs

improve unskolemization

make sure short theorem names are preferred to composite ones in Sledgehammer; this code used to work at some point

properly extract SPASS proof

try out Vampire 11 and parse its output correctly; will revert to Vampire 9 if 11 doesn't perform as well

return updated info record after termination proof

proper context for rule_by_tactic;

conditional warnings: explicitly observe context visibility flag, not just accidental presence of a context; map_ss: explicitly provide a temporary context, which might be required for mksimps, mkcongs etc.;

hgweb style: show author in filelog; full description in annotate hover

proper context for mksimps etc. -- via simpset of the running Simplifier;

read_const: disallow internal names as usual in visible Isar text;

more explicit treatment of context, although not fully localized;

removed some Emacs junk;

merged

make random engine persistent using code_reflect

repaired subtle misunderstanding: statement names are only passed for name resolution

fixed underscore typo

more coherent naming with ML serializer

dropped code_datatype antiquotation

dropped unnecessary ML code

avoid popular infixes

code_reflect: specify module name directly after keyword

NEWS: code_reflect

merged

updated generated file

modernized structure name

use code_reflect

merged