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;