Vampire 3.0 requires types to be declared -- make it happy (and get rid of "implicit" types since only Satallax seems to support them anymore)

whitepsace tuning

more robust parsing of Vampire proofs with "introduced" names

fixed "sorry"d proofs

repaired proofs (after change to xxx_case_def)

temporary sorry's for temporarily nonterminating (due to 2b430bbb5a1a) proofs

qualify intermediate typedefs

avoid double qualification for case constants

qualify more generated names with optional type name component

eliminated bogus assumption from theorem (that was instantiated with refl and resulted in flexflex pairs)

generalized library function

updated keywords;

merged

clarified Query_Operation.register: avoid hard-wired parallel policy; sledgehammer: more conventional parallel exception handling -- print just one interrupt;

moved generic module to its proper place;

manage hyperlinks via PIDE editor interface;

tuned whitespace;

prefer PIDE editor operations; apply_query: insist in non-outdated snapshot via editor.current_command; tuned signature;

central management of Document.Overlays, independent of Document_Model;

tuned -- use Multi_Map;

support for maps with multiple entries per key;

tuned signature;

tuned signature;

tuned signature;

tuned signature -- more abstract PIDE editor operations;

tuned messages

clarified option name (since case/fold/rec are also destructors)

define case constant from other 'free constructor' axioms

introduced case tactics

tuning