use strings to encode type systems in ATP module, to reduce the amount of out-of-place information and also to make it easier to print the type system used

cosmetics

supply type-system defaults for major ATPs

make sure that "file" annotations are read correctly in SInE-E and E proofs

fixed random number invocation

make sure E type information constants are given a weight, even if they don't appear anywhere else

fix ROOT.ML and handle "readable_names" reference slightly more cleanly

show sorts not just types in Isar proofs + tuning

Vampire sometimes generates formulas with ~ (not) followed by a quantified subformula, without parentheses -- parse these correctly

tuning

make SML/NJ happy

added TPTP exporter facility -- useful to do experiments with machine learning

renamed theory to make its purpose clearer

fixing typo

improving naming of fresh variables in OCaml serializer

adding code generation setup for String.implode and String.explode in OCaml (contributed by Andreas Lochbihler)

merged;

modernized rail diagrams using @{rail} antiquotation;

tuning

fixed parsing of multiple negations (e.g. ~~~p) found in Vampire proofs

use "metis", not "metisFT", to reconstruct proofs found in fully-typed mode -- "metisFT" is just too slow...

beware of polymorphic types in typed translation symbol declarations -- match alpha-equivalent types and, more importantly, prevent unsoundnesses by generating type constraints on the arguments of a polymorphic symbols (otherwise "hAPP" can be given any result type)

minor doc fixes

adapt to new type system names

restructured type systems some more -- the old naming schemes had "argshg diff |less" and "tagshg diff |less" as equivalent and didn't support a monomorphic version of "tags"

take "partial_types" option with a grain of salt

fixed SPASS fact offset calculation and report unexpected unsound proofs with so-called sound encodings

close formula universally, to make SPASS happy