a76ace919f1c wasn't quite right; second try

merge

never include anything from the Sledgehammer theory in the relevant facts + killed two obsolete facts

better eta-expansion in Sledgehammer's clausification; make the eta-expansion code more robust in the face of polymorphic arguments + make eta-expansion happen more often, since it first-orderizes things

cosmetics

make sure that theorems passed using "add:" to Sledgehammer are not eliminated on heuristic grounds

improve the new "natural formula" fact filter

explicit treatment of UTF8 sequences as Isabelle symbols;

ML pretty printing of type string according to (quasi-abstract) YXML markup and symbols (including UTF8);

escape UTF8 symbols for the ML compiler;

explicit treatment of UTF8 character sequences as Isabelle symbols;

slight cleaning and simplification of the automatic wrapper for quotient definitions

merged

export of proper information in the ML-interface of the quotient package

treat Pretty.T as strictly abstract type;

slightly more standard data merge: Symtax.merge (K true) avoids equality on abstract type Pretty.T and gracefully accepts overriding, Symtab.join prefers first entry as usual;

avoid equality on abstract type Pretty.T;

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

have "metis" method and "metis_tac" fall back on "metisFT" upon failure, following a suggestion by Larry