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

merged

merged

updated generated files

simplified evaluation function names

turned simp_trace_depth_limit into a configuration option

add notsqsubseteq syntax

show: display goal refinement rule as "state", to avoid odd Output.urgent_message and make its association with the goal more explicit;

make sure errors generated in a thread don't vanish in cyberspace (e.g., when invoking Sledgehammer with unknown facts)

merged

adding postprocessing for maps in term construction of quickcheck; fixed check_all_option definition

added enum_term_of to correct present nested functions

adding postprocessing for sets in term construction of quickcheck

merged

fixed trigger inference: testing if a theorem already has a trigger was too strict; fixed monomorphization with respect to triggers (which might occur schematically)

fixed checking and translation of weights (previously, weights occurring in terms were rejected, and weight numbers were unintended translated into Vars)

the functions term_of and prop_of are also needed in earlier stages, not only for Z3 proof reconstruction, so they really belong in SMT_Utils

facilitate debugging

merged

clean up fudge factors a little bit

added weights to SMT problems

move facts supplied with "add:" to the front, so that they get a better weight (SMT)

beautify MacLaurin proofs; make better use of DERIV_intros

workaround for bug in weight handling -- sometimes numerals got replaced by Vars and this confused the weight extractor

avoid ML structure aliases (especially single-letter abbreviations);

eliminated dead code;

more correct ML snippets that are unchecked; tuned comments;

merged

Added two theorems about the concept of range. Tidied up the comments.

honor "overlord" option for SMT solvers as well and don't pass "ext" to them

make Sledgehammer's relevance filter include the "ext" rule when appropriate

tuning

tuning

added support for "type_sys" option to Mirabelle

honor "metisFT" in Mirabelle

make "full_types" take precedence over "type_sys"

crank up Metis's timeout for SMT solvers, since users love Metis

generate a "using [[smt_solver = ...]]" command if a proof is found by another SMT solver than the current one, to ensure it's also used for reconstruction

make sure first-order occurrences of "False" and "True" are handled correctly -- this broke when adding proper support for higher-order occurrences