notes on packaging;

misc tuning;

tuned auxiliary structures;

Net.encode_type;

more accurate dependencies;

made smlnj happy

fix syntax bug in the TPTP output, by ensuring that "hBOOL" is correctly used for n-ary predicates even if (n + k)-ary occurrences of the same predicate, but with a different type, occur in the same problem

renamed for easier grep

use Skolem inlining also in the nonpolymorphic case, as a step toward simplifying the source code

steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs