src/HOL/Tools/ATP/atp_systems.ML
2012-05-24 blanchet 2012-05-24 update Satallax setup based on evaluation
2012-05-24 blanchet 2012-05-24 gracefully handle definition-looking premises
2012-05-23 blanchet 2012-05-23 tuned names
2012-05-23 blanchet 2012-05-23 improved LEO-II definition handling -- still hoping for a fix directly in LEO-II
2012-05-23 blanchet 2012-05-23 better handling of incomplete TSTP proofs
2012-05-23 blanchet 2012-05-23 lower the monomorphization thresholds for less scalable provers
2012-05-22 blanchet 2012-05-22 added one slice with configurable simplification turned off
2012-05-21 blanchet 2012-05-21 invite users to upgrade their SPASS (so we can get rid of old code)
2012-05-21 blanchet 2012-05-21 start phasing out old SPASS
2012-05-21 blanchet 2012-05-21 minor tweak in Vampire setup
2012-05-16 blanchet 2012-05-16 minor slice tweaking (swapped two slices to move polymorphic encoding up a bit)
2012-05-14 blanchet 2012-05-14 tuning
2012-05-13 blanchet 2012-05-13 LEO-II's "--sos" option confusingly disables rather than enables SOS, and SOS seems to be ignored anyway; also, pass a number of facts that's more appropriate for each prover
2012-05-13 blanchet 2012-05-13 get rid of "conj_sym_kind" -- most interesting provers now have built-in sorts, and for the others (e.g. E) "Hypothesis" isn't too bad a default
2012-05-10 blanchet 2012-05-10 pass fewer facts to LEO-II and Satallax
2012-05-10 blanchet 2012-05-10 tweak LEO-II setup
2012-05-10 blanchet 2012-05-10 use raw monomorphic encoding with Waldmeister, to avoid overloading it with too many function symbols (as would be the case using mangled monomorphic encodings)
2012-04-27 blanchet 2012-04-27 tweak LEO-II setup
2012-04-26 blanchet 2012-04-26 tentatively tag hypotheses as definition -- this sometimes help the "tptp_sledgehammer" tool (e.g. SEU466^1.p)
2012-04-24 blanchet 2012-04-24 removed confusing error
2012-04-22 blanchet 2012-04-22 tried harder to make SML/NJ happy
2012-04-21 blanchet 2012-04-21 tried to make SML/NJ happy
2012-04-19 blanchet 2012-04-19 true delayed evaluation of "SPASS_VERSION" environment variable
2012-04-17 blanchet 2012-04-17 more helpful error message
2012-04-17 blanchet 2012-04-17 avoid option introduced in E 1.2 when invoking older versions of E
2012-04-16 wenzelm 2012-04-16 redirect bash stderr to Isabelle warning as appropriate -- avoid raw process error output which may either get ignored or overload PIDE syslog in extreme cases;
2012-03-27 blanchet 2012-03-27 tweak slices, based on eval by Daniel Wand
2012-03-21 blanchet 2012-03-21 removed Satallax option, now that this is the default
2012-03-21 blanchet 2012-03-21 improve "remote_satallax" by exploiting unsat core
2012-03-21 blanchet 2012-03-21 generate weights and precedences for predicates as well
2012-03-20 blanchet 2012-03-20 made "spass" a "metaprover" that uses either the new SPASS or the old SPASS, to preserve backward compatibility and prepare for the upcoming release
2012-03-20 blanchet 2012-03-20 tweaks
2012-03-20 blanchet 2012-03-20 added term_order option to Mirabelle
2012-03-20 blanchet 2012-03-20 added "metis_advisory_simp" option to orient as many equations as possible in Metis the right way (cf. "More SPASS with Isabelle")
2012-03-20 blanchet 2012-03-20 continued implementation of term ordering attributes
2012-03-20 blanchet 2012-03-20 implement term order attribute (for experiments)
2012-03-20 blanchet 2012-03-20 tuning -- don't refer to old, internal version number (needlessly confusing now)
2012-03-20 blanchet 2012-03-20 more weight attribute tuning
2012-03-20 blanchet 2012-03-20 use TFF0 with remote Vampire, now that a newer version of Vampire has been installed there (1.8 rev. 1362) that appears to have sound support for TFF0
2012-03-20 blanchet 2012-03-20 internal renamings
2012-03-20 blanchet 2012-03-20 renamed E weight attribute
2012-02-24 blanchet 2012-02-24 added support for Alt-Ergo through Why3 (mostly for experimental purposes, e.g. polymorphism vs. monomorphization)
2012-02-14 blanchet 2012-02-14 don't report spurious LEO-II errors
2012-02-14 blanchet 2012-02-14 better error message
2012-02-11 blanchet 2012-02-11 new SPASS options
2012-02-10 blanchet 2012-02-10 update SPASS slices
2012-02-09 blanchet 2012-02-09 new SPASS slices
2012-02-06 blanchet 2012-02-06 renamed type encoding
2012-02-05 blanchet 2012-02-05 remove option that's on by default
2012-02-05 blanchet 2012-02-05 no need for a script/mega-hack with the new SPASS
2012-02-05 blanchet 2012-02-05 cleaned up new SPASS parsing
2012-02-04 blanchet 2012-02-04 made option available to users (mostly for experiments)
2012-02-03 blanchet 2012-02-03 optimization: slice caching in case two consecutive slices are nearly identical
2012-02-02 blanchet 2012-02-02 change 9ce354a77908 wasn't quite right -- here's an improvement
2012-02-02 blanchet 2012-02-02 better SPASS setup
2012-02-02 blanchet 2012-02-02 include new SPASS by default if available
2012-01-31 blanchet 2012-01-31 third attempt at lambda lifting that works for both Sledgehammer and Metis (cf. dce6c3a460a9)
2012-01-31 blanchet 2012-01-31 improve SPASS setup
2012-01-31 blanchet 2012-01-31 fixed syntax bug in DFG output
2012-01-31 blanchet 2012-01-31 new SPASS setup