proper constants in TPTP $let binding

more operations from Isabelle/ML;

merged

tuned proofs --- eliminated 'guess';

tuned proofs; tuned whitespace;

clarified antiquotations;

proper firstorderization in Sledgehammer

clarified signature; clarified antiquotations;

clarified antiquotations;

clarified signature -- prefer antiquotations (with subtle change of exception content);

more control symbols;

support ML antiquotations with fn abstraction;

unused;

clarified operations: follow Isabelle/ML more closely;

provide current vampire-4.5.1: presently unused in Sledgehammer, but relevant for Isabelle/Naproche;

obsolete;

tuned;

clarified name and options for old vampire-4.2.2;

clarified signature;

explicit predicate for confined bit range avoids cyclic rewriting in presence of extensionality rule for bit values (contributed by Thomas Sewell)

more latex macros;

tuned;

clarified signature;

more antiquotations;