merge

cleaner handling of temporary files

merged

made sml/nj happy

added self-correcting wrapper for Z3 -- see comment in the file for details

impose a limit on the breadth of monomorphization (in addition to on the depth) to prevent an explosion of the number of monomorphic instances

no need to do a super-duper atomization if Metis fails afterwards anyway

removed unused variable

robustly handle SMT exceptions in Sledgehammer

make "debug" imply "blocking", since in blocking mode the exceptions flow through and are more instructive

reintroduce the higher penalty for skolems

tuning

comment tuning

get rid of experimental feature of term patterns in relevance filter -- doesn't work well unless we take into consideration the equality theory entailed by the relevant facts

fixed more issues with the Vampire output parser, and added support for Vampire's TSTP output (--proof tptp)

make it more likely that induction rules are picked up by Sledgehammer

generalize the Vampire parser some more to cope with things like "{2, 3\}" seen in some proofs

add the current theory's constant to the goal to make theorems from the current theory more relevant on the first iteration already

instantiate induction rules automatically

merged

fix lambda-lifting: take level of bound variables into account and also apply bound variables from outer scope

fixed introduction of explicit application function: bound variables always need explicit application if they are applied to some term

fixed eta-expansion: introduce a couple of abstractions at once

merged