fixed the command-line syntax for setting Yices' random seed

merged

updated SMT certificates

fixed lambda-lifting: shift indices of bound variables correctly (after locking the required bound variables) and apply bound variables to the new function symbol in the right order; fixed introduction of explicit application: use explicit application for every additional argument (grouping of arguments caused confusion when translating into the intermediate format)

adding exhaustive tester instances for numeric types: code_numeral, nat, rat and real

updated generated file;

replaced command 'nonterminals' by slightly modernized version 'nonterminal';

renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning;

tuned signature;

clarified exports of structure Simplifier;

refer to regular structure Simplifier;

tuned;

updated SMT certificates

more precise/correct SMT error handling

fixed off-by-one and return proper error code -- never underestimate the number of oddities in Perl

discriminate SMT errors a bit better

keep track of errors in Z3 input file for debugging purposes

better propagation of stdout in case of failure + comply with strict/warnings

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

made sml/nj happy

removing file refute_isar.ML that was missed in 4006f5c3f421

added nitpick to mutabelle script

reactivating nitpick in Mutabelle

more appropriate closures for static evaluation

more uniform naming