src/HOL/Tools/ATP_Manager/atp_systems.ML
2010-06-22 ago removed Sledgehammer's support for the DFG syntax;
2010-06-21 ago thread "full_types"
2010-06-14 ago better error reporting for Vampire
2010-06-14 ago expect SPASS 3.7, and give a friendly warning if an older version is used
2010-06-14 ago improve ATP-specific error messages
2010-06-05 ago show more respect for user-specified facts, even if they could lead to unsound proofs + don't throw away "unsound" theorems in "full_type" mode, since they are then sound
2010-06-05 ago fix remote Vampire diagnosis
2010-06-04 ago recongize one more outcome string for "remote_vampire"
2010-05-28 ago make sure chained facts appear in Isar proofs generated by Sledgehammer -- otherwise the proof won't work
2010-05-17 ago identify common SPASS error more clearly
2010-05-14 ago renamed options
2010-05-14 ago renamed two Sledgehammer options
2010-05-14 ago query _HOME environment variables at run-time, not at build-time
2010-05-14 ago pass "full_type" argument to proof reconstruction
2010-04-29 ago in "overlord" mode: ignore problem prefix specified in the .thy file
2010-04-28 ago back to Vampire 9 -- Vampire 11 sometimes outputs really weird proofs
2010-04-28 ago properly extract SPASS proof
2010-04-28 ago try out Vampire 11 and parse its output correctly;
2010-04-28 ago removed "sorts" option, continued
2010-04-27 ago tuning
2010-04-27 ago remove "higher_order" option from Sledgehammer -- the "smart" default is good enough
2010-04-26 ago rename options and keep track of conjecture shape (to facilitate proof reconstruction)
2010-04-25 ago support readable names even when Isar proof reconstruction is enabled -- useful for debugging
2010-04-23 ago cosmetics
2010-04-23 ago now rename the file "atp_wrapper.ML" to "atp_systems.ML" + fix typo in "SystemOnTPTP" script