update the Vampire related parts of the documentation

fixed TFF slicing

kindly ask Vampire to output axiom names

added formats to the slice and use TFF for remote Vampire

tuned specifications, syntax and proofs

tuned specifications and syntax

Quotient Package: some infrastructure for lifting inside sets

include all encodings in tests, now that the incompleteness of some encodings has been addressed

change Metis's default settings if type information axioms are generated

we must tag any type whose ground types intersect a nonmonotonic type

prefer the lighter, slightly unsound monotonicity-based encodings for Metis

made reconstruction of type tag equalities "\?x = \?x" reliable

tuning ATP problem output

revert guard logic -- make sure that typing information is generated for existentials

generate tag equations for existential variables

tuning, plus started implementing tag equation generation for existential variables

precisely distinguish between universal and existential quantifiers, instead of assuming the worst (universal), for monotonicity analysis

clearer terminology

renamed "heavy" to "uniform", based on discussion with Nick Smallbone

removed unused configuration option

added caching for (in)finiteness checks

remove needless typing information

cleaner handling of polymorphic monotonicity inference

started cleaning up polymorphic monotonicity-based encodings, based on discussions with Nick Smallbone

more precise warning

added option to control soundness of encodings more precisely, for evaluation purposes

make sound mode more sound (and clean up code)

reintroduced slightly unsound optimization taken out in 717880e98e6b, but only if "sound" is false

gracefully handle empty SPASS problems

pass sound option to Sledgehammer tactic

tuned signature -- contrast physical output primitives versus Output.raw_message;

tuned signature;

discontinued slightly odd Future/Lazy.get_finished, which do not really fit into the execution model of Future.cancel/join_tasks (canceled tasks need to be dequeued and terminated explicitly);

some support for toplevel printing wrt. editor perspective (still inactive);

propagate editor perspective through document model;

some support for editor perspective;

discontinued redundant Edit_Command_ID;

reduced warnings;

tuned message;

old-style numbered structure index is legacy feature (hardly ever used now);

added official Text.Range.Ordering; some support for text perspective;

tuned signature;

reverted some odd changes to HOL/Import (cf. 74c08021ab2e);

merged

modernized specifications

removed session HOL/Subst -- now subsumed my more modern HOL/ex/Unification.thy

removed technical or trivial unused facts

more precise authors and comments; tuned order and headers

added proof of idempotence, roughly after HOL/Subst/Unify.thy

tuned proofs, sledgehammering overly verbose parts

tuned notation

ported some lemmas from HOL/Subst/*; tuned order

changed constant names and notation to match HOL/Subst/*.thy, from which this theory is a clone.

merged

add lemmas interior_Times and closure_Times

avoid pred/set mixture

avoid pred/set mixture

merged

remove unnecessary euclidean_space class constraints

section -> subsection