src/HOL/ATP.thy
Thu, 10 Dec 2020 19:08:12 +0100 desharna tuned name generation in tptp to not depend on shadowing
Thu, 12 Nov 2020 17:42:15 +0100 desharna Removed development code wrongfully committed
Thu, 05 Nov 2020 18:14:02 +0100 desharna Added support for TFX to Sledgehammer
Thu, 08 Oct 2020 16:36:00 +0200 desharna drop obsolete ad hoc support for Satallax isar proof reconstruction
Thu, 23 Apr 2020 15:45:42 +0200 blanchet tweaked Vampire's options + tuning
Fri, 25 Oct 2019 16:28:04 +0200 blanchet compile
Fri, 25 Oct 2019 14:55:14 +0200 blanchet removed E-SInE, a very old system by now (and SInE has been incorporated in many provers in the past decade)
Fri, 25 Oct 2019 14:14:56 +0200 blanchet removed experimental encoding for Waldmeister
Sun, 06 Jan 2019 15:04:34 +0100 wenzelm isabelle update -u path_cartouches;
Mon, 07 Aug 2017 11:21:11 +0200 blanchet tuning imports
Sat, 18 Jul 2015 22:58:50 +0200 wenzelm isabelle update_cartouches;
Sun, 02 Nov 2014 18:21:45 +0100 wenzelm modernized header uniformly as section;
Sat, 20 Sep 2014 10:44:24 +0200 steckerm Changed proof method to auto for custom Waldmeister lemma
Sat, 20 Sep 2014 10:44:24 +0200 steckerm Minor fixes in ATP_Waldmeister
Tue, 02 Sep 2014 16:38:26 +0200 steckerm Some work on the new waldmeister integration
Wed, 30 Jul 2014 14:03:13 +0200 fleury Changing the role of rule "tmp_ite_elim" of the SMT solver veriT to Lemma.
Wed, 30 Jul 2014 14:03:12 +0200 fleury imported patch hilbert_choice_support
Wed, 30 Jul 2014 14:03:12 +0200 fleury imported patch satallax_proof_support_Sledgehammer
Mon, 16 Jun 2014 19:40:59 +0200 blanchet simplified code
Mon, 16 Jun 2014 19:40:04 +0200 blanchet moved code around
Mon, 16 Jun 2014 16:18:15 +0200 fleury add support for Isar reconstruction for thf1 ATP provers like Leo-II.
Tue, 13 May 2014 11:10:23 +0200 blanchet hide more internal names
Fri, 18 Oct 2013 10:43:21 +0200 blanchet killed more "no_atp"s
Mon, 09 Sep 2013 15:22:04 +0200 blanchet move metis to new monomorphizer
Thu, 28 Mar 2013 23:44:41 +0100 boehmes new, simpler implementation of monomorphization;
Wed, 22 Aug 2012 22:55:41 +0200 wenzelm prefer ML_file over old uses;
Mon, 21 May 2012 10:39:32 +0200 blanchet add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
Mon, 23 Jan 2012 17:40:32 +0100 blanchet renamed two files to make room for a new file
Wed, 14 Dec 2011 18:07:32 +0100 blanchet added new proof redirection code
Wed, 16 Nov 2011 17:19:08 +0100 blanchet compile
Tue, 09 Aug 2011 09:05:21 +0200 blanchet load lambda-lifting structure earlier, so it can be used in Metis
Tue, 05 Jul 2011 17:09:59 +0100 nik improved translation of lambdas in THF
Tue, 31 May 2011 16:38:36 +0200 blanchet use "monomorph.ML" in "ATP" theory (so the new Metis can use it)
Tue, 31 May 2011 16:38:36 +0200 blanchet first step in sharing more code between ATP and Metis translation
Tue, 26 Oct 2010 12:17:19 +0200 blanchet reverted e7a80c6752c9 -- there's not much point in putting a diagnosis tool (as opposed to a proof method) in Plain, but more importantly Sledgehammer must be in Main to use SMT solvers
Mon, 25 Oct 2010 13:34:57 +0200 haftmann moved sledgehammer to Plain; tuned dependencies
Tue, 05 Oct 2010 12:50:45 +0200 blanchet tuned comments
Tue, 05 Oct 2010 11:10:37 +0200 blanchet factor out "ATP" from "Sledgehammer" (cf. "SAT" vs. "Refute", etc.) -- the theories now reflect the directory structure
less more (0) tip