Tue, 07 Jun 2011 11:12:52 +0200 blanchet tuning
Tue, 07 Jun 2011 11:05:09 +0200 blanchet merged
Tue, 07 Jun 2011 11:04:17 +0200 blanchet use the proper prover name, e.g. metis_full_types, not metis (full_types), for minimizing
Tue, 07 Jun 2011 10:46:09 +0200 blanchet removed "verbose" option -- there won't be any verbosity in there, according to Sascha (yeah)
Tue, 07 Jun 2011 10:43:18 +0200 blanchet nicely thread monomorphism verbosity in Metis and Sledgehammer
Tue, 07 Jun 2011 10:24:16 +0200 boehmes clarified meaning of monomorphization configuration option by renaming it
Tue, 07 Jun 2011 08:58:23 +0200 blanchet documentation tweaks
Tue, 07 Jun 2011 08:52:35 +0200 blanchet obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
Tue, 07 Jun 2011 07:57:24 +0200 blanchet fixed typo in legacy feature message
Tue, 07 Jun 2011 07:45:12 +0200 blanchet use new monomorphization code
Tue, 07 Jun 2011 07:44:54 +0200 blanchet added (currently unused) verbose configuration option
Tue, 07 Jun 2011 07:06:24 +0200 blanchet renamed ML function
Tue, 07 Jun 2011 07:04:53 +0200 blanchet renamed example theory to "ATP_Export", for consistency with its underlying "ATP_" modules
Tue, 07 Jun 2011 06:58:52 +0200 blanchet pass props not thms to ATP translator
Mon, 06 Jun 2011 23:46:02 +0200 blanchet slighly more reasonable Vampire slices (until new monomorphizer is used)
Mon, 06 Jun 2011 23:43:28 +0200 blanchet removed confusing slicing logic
Mon, 06 Jun 2011 23:26:40 +0200 blanchet suggest first reconstructor that timed out, not last (i.e. metis not metisFT in most cases)
Mon, 06 Jun 2011 23:11:14 +0200 blanchet effectively reenable slices for SPASS and Vampire -- they were disabled by mistake
Mon, 06 Jun 2011 22:03:58 +0200 blanchet minor: curly brackets, not square brackets
Mon, 06 Jun 2011 21:58:29 +0200 blanchet document metis better in Sledgehammer docs
Mon, 06 Jun 2011 21:02:24 +0200 blanchet updated Sledgehammer message
Mon, 06 Jun 2011 20:56:06 +0200 blanchet removed old optimization that isn't one anyone
Mon, 06 Jun 2011 20:56:06 +0200 blanchet generate less type information in polymorphic case
Mon, 06 Jun 2011 20:56:06 +0200 blanchet Metis code cleanup
Mon, 06 Jun 2011 20:36:36 +0200 blanchet enable new Metis
Mon, 06 Jun 2011 20:36:35 +0200 blanchet made "explicit_apply"'s smart mode (more) complete
Mon, 06 Jun 2011 20:36:35 +0200 blanchet fall back in case path finder fails -- these errors are sometimes salvageable
Mon, 06 Jun 2011 20:36:35 +0200 blanchet compile
Mon, 06 Jun 2011 20:36:35 +0200 blanchet 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"
Mon, 06 Jun 2011 20:36:35 +0200 blanchet marked "metisF" as legacy -- nobody uses it or needs it
Mon, 06 Jun 2011 20:36:35 +0200 blanchet more preparations towards hijacking Metis
Mon, 06 Jun 2011 20:36:35 +0200 blanchet remove more occurrences of "metisX", preparing for the D Day when it will silently hijack "metis" and "metisFT"
Mon, 06 Jun 2011 20:36:35 +0200 blanchet don't mention "metisX" so much in the docs -- it will go away soon
Mon, 06 Jun 2011 20:36:35 +0200 blanchet reintroduced metisFT in example
Mon, 06 Jun 2011 20:36:35 +0200 blanchet make "smart" mode of "explicit_apply" smarter, by also detecting the other kind of higher-order quantification, namely "bool"s
Mon, 06 Jun 2011 20:36:35 +0200 blanchet imported patch metis_reconstr_give_type_infer_a_chance
Mon, 06 Jun 2011 20:36:35 +0200 blanchet make "metisX"'s default more like old "metis"
Mon, 06 Jun 2011 20:36:35 +0200 blanchet whitespace tuning
Mon, 06 Jun 2011 20:36:35 +0200 blanchet tuned Metis examples
Mon, 06 Jun 2011 20:36:35 +0200 blanchet more through tests of new Metis
Mon, 06 Jun 2011 20:36:35 +0200 blanchet improved correctness of handling of higher-order occurrences of "Not" in new Metis (and probably in old Metis)
Mon, 06 Jun 2011 20:36:35 +0200 blanchet fixed type helper indices in new Metis
Mon, 06 Jun 2011 20:36:35 +0200 blanchet improved ATP clausifier so it can deal with "x => (y <=> z)"
Mon, 06 Jun 2011 20:36:35 +0200 blanchet avoid renumbering hypotheses
Mon, 06 Jun 2011 20:36:35 +0200 blanchet fixed reconstruction of new Skolem constants in new Metis
Mon, 06 Jun 2011 20:36:35 +0200 blanchet don't translate new Skolemizer assumptions in new Metis
Mon, 06 Jun 2011 20:36:35 +0200 blanchet tuning
Mon, 06 Jun 2011 20:36:35 +0200 blanchet fixed detection of Skolem constants in type construction detection code
Mon, 06 Jun 2011 20:36:35 +0200 blanchet 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)
Mon, 06 Jun 2011 20:36:35 +0200 blanchet tuning
Mon, 06 Jun 2011 20:36:35 +0200 blanchet also exploit type tag idempotence in lightweight encodings, following a suggestion from Gothenburg
Mon, 06 Jun 2011 20:36:35 +0200 blanchet reveal Skolems in new Metis
Mon, 06 Jun 2011 20:36:35 +0200 blanchet don't throw exception on unknown constants (e.g. skolems), and give more precise type to applied functions
Mon, 06 Jun 2011 20:36:35 +0200 blanchet slacker version of "fastype_of", in case a function has dummy type
Mon, 06 Jun 2011 20:36:35 +0200 blanchet don't stumble on Skolem names
Mon, 06 Jun 2011 20:36:35 +0200 blanchet conceal old Skolems in new Metis
Mon, 06 Jun 2011 20:36:35 +0200 blanchet 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
Mon, 06 Jun 2011 20:36:35 +0200 blanchet use "" type only in THF and TFF -- might cause strange failures if used in FOF or CNF, depending on how liberal the prover is
Mon, 06 Jun 2011 20:36:35 +0200 blanchet properly unmangle names in path finder
Mon, 06 Jun 2011 20:36:35 +0200 blanchet only uncombine combinators in textual Isar proofs, not in Metis
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip