src/HOL/Tools/ATP/atp_systems.ML
2013-05-26 blanchet 2013-05-26 disable SPASS's splitting if Isar proofs are desired, because these are not handled by the proof reconstruction code (and it's not clear how to handle them considering the lack of documentation)
2013-05-21 blanchet 2013-05-21 disabled choice in Satallax
2013-05-21 blanchet 2013-05-21 prefer compiled version of LEO-II and Satallax if available
2013-05-21 blanchet 2013-05-21 updated remote provers
2013-05-20 blanchet 2013-05-20 started adding agsyHOL as an experimental prover
2013-05-15 blanchet 2013-05-15 renamed Sledgehammer functions with 'for' in their names to 'of'
2013-05-08 blanchet 2013-05-08 use right default for "uncurried_aliases" with polymorphic SPASS
2013-05-03 blanchet 2013-05-03 tuning
2013-05-03 blanchet 2013-05-03 pass certain readability-enhancing Vampire options only when an Isar proof is needed
2013-04-08 blanchet 2013-04-08 robustness w.r.t. unknown arguments
2013-03-20 blanchet 2013-03-20 use the right role for SPASS hypotheses
2013-03-05 blanchet 2013-03-05 polymorphic SPASS is also SPASS
2013-02-21 blanchet 2013-02-21 swap slices so that the last slice is more complete (for minimization)
2013-02-20 blanchet 2013-02-20 upgraded to Alt-Ergo 0.95
2013-02-20 blanchet 2013-02-20 turn off more evil Vampire options to facilitate Isar proof generation
2013-02-03 blanchet 2013-02-03 tuned slicing (E-MaLeS and E-Par)
2013-02-02 blanchet 2013-02-02 tune slices further
2013-02-02 blanchet 2013-02-02 tweak ATP slices further
2013-01-31 blanchet 2013-01-31 tuned slices
2013-01-31 blanchet 2013-01-31 store fact filter along with ATP slice
2013-01-17 blanchet 2013-01-17 make SPASS more configurable, for experiments
2013-01-17 blanchet 2013-01-17 added E-Par support
2012-12-03 blanchet 2012-12-03 tweak SPASS default a tiny bit, so that a more interesting heuristic is chosen when "slicing=false" (for experiments)
2012-10-31 blanchet 2012-10-31 less verbose -- the warning will reach the users anyway by other means
2012-10-31 blanchet 2012-10-31 tuned messages
2012-10-31 blanchet 2012-10-31 added a timeout around script that relies on the network
2012-10-31 blanchet 2012-10-31 tuning
2012-08-14 blanchet 2012-08-14 tone down "z3_tptp", now that Z3 (starting with 4.1) no longer supports TPTP TFF0
2012-08-14 blanchet 2012-08-14 tweak Vampire setup in the light of new evaluation
2012-08-07 blanchet 2012-08-07 proper quoting
2012-08-07 blanchet 2012-08-07 stop distinguishing between complete and incomplete slices, since this is very fragile and has hardly any useful semantics to users
2012-08-07 blanchet 2012-08-07 specify full path to clausifier
2012-08-06 blanchet 2012-08-06 added iProver(-Eq) local
2012-08-02 blanchet 2012-08-02 support older versions of Vampire
2012-08-02 blanchet 2012-08-02 added E-MaLeS to list of provers for testing
2012-07-27 blanchet 2012-07-27 tweaks in preparation for type encoding evaluation
2012-07-27 blanchet 2012-07-27 extract Z3 unsat cores (for "z3_tptp")
2012-07-20 blanchet 2012-07-20 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
2012-07-10 blanchet 2012-07-10 don't ask E to generate a detailed proofs if not needed
2012-06-26 blanchet 2012-06-26 started adding polymophic SPASS output
2012-06-26 blanchet 2012-06-26 tuning
2012-06-26 blanchet 2012-06-26 removed support for unsorted DFG, now that SPASS 3.7 is no longer supported
2012-06-06 blanchet 2012-06-06 pass more facts to LEO-II, in the light of latest evaluation
2012-06-06 blanchet 2012-06-06 robust LEO-II setup that doesn't rely on ".leoatprc"
2012-06-06 blanchet 2012-06-06 tweaked remote Vampire version
2012-05-28 blanchet 2012-05-28 tweaked remote Vampire setup
2012-05-28 blanchet 2012-05-28 killed SPASS 3.5/3.7 FLOTTER hack -- requires users to upgrade to SPASS 3.8
2012-05-28 blanchet 2012-05-28 don't generate definitions for LEO-II -- this cuases more harm than good
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