don't needlessly extensionalize

don't needlessly presimplify -- makes ATP problem preparation much faster

tuned

removed experimental code submitted by mistake

make sure that the message tail (timing + TPTP important message) is preserved upon automatic minimization

removed removed option from documentation

killed "explicit_apply" option in Sledgehammer -- the "smart" default is about as lightweight as "false" and just as complete as "true"

slightly faster/cleaner accumulation of polymorphic consts

eliminated unnecessary tail-recursion and funny use of records as 'named arguments' for functions

more conventional variable naming

dropped outdated/speculative historical comments; adapted to isabelle commenting style; tuned

less redundant tags

removed generation of instantiated pattern set, which is never actually used

more precise type for obscure "prfx" field

clarified (and slightly modified) the semantics of max_new_instances

use null_heap instead of %_. 0 to avoid printing problems

prioritize more relevant facts for monomorphization

more suitable implementation of "schematic_consts_of" for monomorphizer, for ATPs

workaround current "max_new_instances" semantics

fixed missing proof handling

optimized the relevance filter a little bit

printing environment in mutabelle's log

merged

merged; manually merged IsaMakefile

splitting Cset into Cset and List_Cset

adding finitize_functions and processing of equivalences in existential compilation in quickcheck_narrowing

adding examples with existentials

renaming the formalisation of the birthday problem to a proper English name

adding compilation that allows existentials in Quickcheck_Narrowing

move away from old SMT monomorphizer

tuning

merged

use the proper prover name, e.g. metis_full_types, not metis (full_types), for minimizing

removed "verbose" option -- there won't be any verbosity in there, according to Sascha (yeah)

nicely thread monomorphism verbosity in Metis and Sledgehammer

clarified meaning of monomorphization configuration option by renaming it

documentation tweaks

obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be

fixed typo in legacy feature message

use new monomorphization code

added (currently unused) verbose configuration option

renamed ML function

renamed example theory to "ATP_Export", for consistency with its underlying "ATP_" modules

pass props not thms to ATP translator

slighly more reasonable Vampire slices (until new monomorphizer is used)

removed confusing slicing logic

suggest first reconstructor that timed out, not last (i.e. metis not metisFT in most cases)

effectively reenable slices for SPASS and Vampire -- they were disabled by mistake

minor: curly brackets, not square brackets

document metis better in Sledgehammer docs

updated Sledgehammer message

removed old optimization that isn't one anyone

generate less type information in polymorphic case

Metis code cleanup

enable new Metis

made "explicit_apply"'s smart mode (more) complete

fall back in case path finder fails -- these errors are sometimes salvageable

compile

change var name as a workaround for rare issue in Metis's reconstruction code -- namely, "find_var" fails because "X = X" is wrongly mirrorred as "A = A"

marked "metisF" as legacy -- nobody uses it or needs it

more preparations towards hijacking Metis

remove more occurrences of "metisX", preparing for the D Day when it will silently hijack "metis" and "metisFT"

don't mention "metisX" so much in the docs -- it will go away soon

reintroduced metisFT in example

make "smart" mode of "explicit_apply" smarter, by also detecting the other kind of higher-order quantification, namely "bool"s

imported patch metis_reconstr_give_type_infer_a_chance

make "metisX"'s default more like old "metis"

whitespace tuning

tuned Metis examples

more through tests of new Metis

improved correctness of handling of higher-order occurrences of "Not" in new Metis (and probably in old Metis)

fixed type helper indices in new Metis

improved ATP clausifier so it can deal with "x => (y <=> z)"

avoid renumbering hypotheses

fixed reconstruction of new Skolem constants in new Metis

don't translate new Skolemizer assumptions in new Metis

tuning

fixed detection of Skolem constants in type construction detection code

make resolution replay more robust, in case Metis distinguishes between two literals that are merged in Isabelle (e.g. because they carry more or less type annotations in Metis)

tuning

also exploit type tag idempotence in lightweight encodings, following a suggestion from Gothenburg

reveal Skolems in new Metis

don't throw exception on unknown constants (e.g. skolems), and give more precise type to applied functions

slacker version of "fastype_of", in case a function has dummy type

don't stumble on Skolem names

conceal old Skolems in new Metis

don't merge "hAPP"s even in unsound heavy modes, because "hAPP" then sometimes gets declared with too strict arguments ("ind"), and we lose some proofs

use "" type only in THF and TFF -- might cause strange failures if used in FOF or CNF, depending on how liberal the prover is

properly unmangle names in path finder

only uncombine combinators in textual Isar proofs, not in Metis

properly locate helpers whose constants have several entries in the helper table

skip "hBOOL" in new Metis path finder

don't pass "~ " to new Metis

tuning

gracefully handle the case where a constant is partially or not instantiated at all, as may happen when reconstructing Metis proofs for polymorphic type encodings

temporarily document "metisX"