src/HOL/Sledgehammer.thy
2022-03-25 blanchet cleaned up obsolete E setup and a bit of SPASS
2022-03-25 blanchet second and last step in making time slicing more flexible in Sledgehammer: try to honor desired slice size
2022-01-31 blanchet update slice options centrally
2022-01-31 blanchet further work on new Sledgehammer slicing
2022-01-31 blanchet tweaked verbose output
2022-01-31 blanchet tweak padding of prover slice schedule to include all provers
2022-01-31 blanchet implemented 'max_proofs' mechanism
2022-01-31 blanchet document new option 'max_proofs'
2022-01-31 blanchet crude implementation of centralized slicing
2021-05-12 wenzelm avoid duplicate loading of ML file;
2021-03-12 wenzelm support for SystemOnTPTP in Isabelle/ML and Isabelle/Scala (without perl);
2020-11-12 desharna Removed development code wrongfully committed
2020-11-05 desharna Added support for TFX to Sledgehammer
2020-10-08 blanchet removed support for obsolete prover SNARK and underperforming prover E-Par
2020-10-08 desharna tune filename
2020-09-08 desharna [mirabelle] add initial documentation in Sledgehammer's doc
2020-04-23 blanchet tweaked Vampire's options + tuning
2019-10-25 blanchet compile
2019-10-25 blanchet removed E-SInE, a very old system by now (and SInE has been incorporated in many provers in the past decade)
2019-01-06 wenzelm isabelle update -u path_cartouches;
2016-07-11 wenzelm tuned;
2015-07-18 wenzelm isabelle update_cartouches;
2015-01-29 wenzelm more explicit indication of Async_Manager_Legacy as Proof General legacy;
2014-11-02 wenzelm modernized header uniformly as section;
2014-09-29 blanchet made 'moura' tactic more powerful
2014-08-28 blanchet moved skolem method
2014-08-28 blanchet added 'skolem' method, esp. for 'obtain's generated from Z3 proofs
2014-08-27 blanchet renamed new SMT module from 'SMT2' to 'SMT'
2014-06-16 blanchet fixed parsing of one-argument 'file()' in TSTP files
2014-06-16 blanchet use right delimiters for Waldmeister proofs
2014-06-16 blanchet simplified code
2014-06-16 blanchet moved code around
2014-06-12 blanchet tuned dependencies
2014-06-11 blanchet reduces Sledgehammer dependencies
2014-06-11 blanchet moved new highly experimental Waldmeister-specific code (authored by Albert Steckermeier) into Isabelle
2014-06-11 blanchet removed old SMT module from Sledgehammer
2014-03-14 blanchet undo rewrite rules (e.g. for 'fun_app') in Isar
2014-03-14 blanchet more simplification of trivial steps
2014-03-13 blanchet integrate SMT2 with Sledgehammer
2014-03-13 blanchet moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
2014-02-03 blanchet renamed ML file
2014-02-03 blanchet got rid of 'try0' step that is now redundant
2014-01-31 blanchet moved ML code around
2014-01-31 blanchet refactor large ML file
2014-01-31 blanchet renamed many Sledgehammer ML files to clarify structure
2014-01-31 blanchet renamed ML file
2014-01-31 blanchet tuned ML file name
2013-12-20 blanchet reconstruct SPASS-Pirate steps of the form 'x ~= C x' (or more complicated)
2013-07-12 wenzelm hybrid "auto" tool setup, for TTY (within theory) and PIDE (global print function);
2013-07-12 smolkas minimize dependencies (used facts) of Isar proof steps; remove unreferenced steps
2013-07-11 smolkas optimize isar-proofs by trying different proof methods
2013-07-09 smolkas moved code -> easier debugging
2013-02-18 smolkas split isar_step into isar_step, fix, assms; made isar_proof explicit; register fixed variables in ctxt and auto_fix terms to avoid superfluous annotations
2013-02-18 smolkas simplified byline, isar_qualifier
2013-02-14 smolkas renamed sledgehammer_shrink to sledgehammer_compress
2013-01-17 smolkas move preplaying to own structure
2012-11-28 smolkas renamed sledgehammer_isar_reconstruct to sledgehammer_proof
2012-11-28 smolkas put shrink in own structure
2012-11-28 smolkas put annotate in own structure
2012-10-16 blanchet added proof minimization code from Steffen Smolka
less more (0) -100 -60 tip