Mercurial Mercurial > repos > isabelle / file revisions
summary | shortlog | changelog | graph | tags | bookmarks | branches | file | revisions | annotate | diff | comparison | rss | help
(0) tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML
Mon, 28 Mar 2016 12:05:47 +0200 blanchet refined experimental option of Sledgehammer file | diff | annotate
Mon, 07 Mar 2016 21:09:28 +0100 wenzelm File.bash_string operations in ML as in Scala -- exclusively for GNU bash, not perl and not user output; file | diff | annotate
Sat, 05 Mar 2016 17:01:45 +0100 wenzelm tuned signature -- clarified modules; file | diff | annotate
Tue, 23 Feb 2016 16:41:14 +0100 nipkow more canonical names file | diff | annotate
Sat, 19 Dec 2015 20:02:51 +0100 blanchet cleaner generation of metainformation in DFG format and TPTP theory exporter for Sledgehammer file | diff | annotate
Mon, 05 Oct 2015 21:46:48 +0200 blanchet added "!=" (disequality) as a TPTP binary operator, since it pops up in LEO-II proofs file | diff | annotate
Wed, 19 Aug 2015 20:41:23 +0200 wenzelm proper check for Windows executables; file | diff | annotate
Thu, 13 Aug 2015 11:05:19 +0200 wenzelm tuned signature, in accordance to sortBy in Scala; file | diff | annotate
Wed, 04 Mar 2015 19:53:18 +0100 wenzelm tuned signature -- prefer qualified names; file | diff | annotate
Tue, 03 Mar 2015 16:37:45 +0100 blanchet SPASS-Pirate is now called Pirate file | diff | annotate
Mon, 22 Dec 2014 14:33:53 +0100 wenzelm separate module Random; file | diff | annotate
Fri, 31 Oct 2014 11:36:41 +0100 wenzelm discontinued obsolete Output.urgent_message; file | diff | annotate
Tue, 09 Sep 2014 15:33:01 +0200 steckerm Fixed bug which broke isar proof construction for all ATPs except Waldmeister_new file | diff | annotate
Tue, 02 Sep 2014 16:38:26 +0200 steckerm Some work on the new waldmeister integration file | diff | annotate
Thu, 28 Aug 2014 16:58:27 +0200 blanchet merged minimize and auto_minimize file | diff | annotate
Tue, 05 Aug 2014 09:20:00 +0200 blanchet tuning file | diff | annotate
Mon, 04 Aug 2014 13:06:24 +0200 blanchet default on 'metis' for ATPs if preplaying is disabled file | diff | annotate
Mon, 04 Aug 2014 12:28:42 +0200 blanchet rationalized sorting of facts -- so that preplaying (almost always) coincides with the real thing, preventing odd failures file | diff | annotate
Fri, 01 Aug 2014 14:43:57 +0200 blanchet restored a bit of laziness file | diff | annotate
Fri, 01 Aug 2014 14:43:57 +0200 blanchet honor 'try0' also for one-liners file | diff | annotate
Fri, 01 Aug 2014 14:43:57 +0200 blanchet tuning file | diff | annotate
Fri, 01 Aug 2014 14:43:57 +0200 blanchet eliminated needlessly complex message tail file | diff | annotate
Fri, 01 Aug 2014 14:43:57 +0200 blanchet eliminated Sledgehammer's "min" subcommand (and lots of complications in the code) file | diff | annotate
Fri, 01 Aug 2014 14:43:57 +0200 blanchet rationalized preplaying by eliminating (now superfluous) laziness file | diff | annotate
Fri, 01 Aug 2014 14:43:57 +0200 blanchet simplified minimization logic file | diff | annotate
Wed, 30 Jul 2014 23:52:56 +0200 blanchet use parallel preplay machinery also for one-line proofs file | diff | annotate
Wed, 30 Jul 2014 23:52:56 +0200 blanchet always minimize Sledgehammer results by default file | diff | annotate
Wed, 30 Jul 2014 14:03:12 +0200 fleury imported patch satallax_proof_support_Sledgehammer file | diff | annotate
Fri, 25 Jul 2014 11:26:17 +0200 blanchet avoid 'eproof' and 'eproof_ram' scripts if possible (i.e. if 'eprover' can produce reasonable enough proofs for one-liner reconstruction) file | diff | annotate
Tue, 01 Jul 2014 16:47:10 +0200 blanchet speed up MaSh a bit file | diff | annotate
Mon, 16 Jun 2014 19:42:44 +0200 blanchet integrated new Waldmeister code with 'sledgehammer' command file | diff | annotate
Mon, 16 Jun 2014 19:41:42 +0200 blanchet fixed parsing of one-argument 'file()' in TSTP files file | diff | annotate
Mon, 16 Jun 2014 19:40:59 +0200 blanchet simplified code file | diff | annotate
Mon, 16 Jun 2014 16:21:52 +0200 fleury Moving the remote prefix deleting on Sledgehammer's side file | diff | annotate
Mon, 16 Jun 2014 16:18:15 +0200 fleury add support for Isar reconstruction for thf1 ATP provers like Leo-II. file | diff | annotate
Thu, 12 Jun 2014 17:10:12 +0200 blanchet renamed Sledgehammer options file | diff | annotate
Mon, 02 Jun 2014 15:10:18 +0200 fleury basic setup for zipperposition prover file | diff | annotate
Thu, 22 May 2014 03:29:36 +0200 blanchet tuning file | diff | annotate
Fri, 21 Mar 2014 20:33:56 +0100 wenzelm more qualified names; file | diff | annotate
Thu, 13 Feb 2014 13:16:17 +0100 blanchet avoid changing the state's context -- this results in transfer problems later with SMT, and hence preplay tactic failures file | diff | annotate
Mon, 03 Feb 2014 23:38:33 +0100 blanchet properly overwrite replay data from one compression iteration to another file | diff | annotate
Mon, 03 Feb 2014 23:20:12 +0100 blanchet tuning file | diff | annotate
Mon, 03 Feb 2014 19:32:02 +0100 blanchet renamed 'smt' option 'smt_proofs' to avoid clash with 'smt' prover file | diff | annotate
Mon, 03 Feb 2014 19:32:02 +0100 blanchet tuned behavior of 'smt' option file | diff | annotate
Mon, 03 Feb 2014 17:13:31 +0100 blanchet added 'smt' option to control generation of 'by smt' proofs file | diff | annotate
Mon, 03 Feb 2014 16:53:58 +0100 blanchet renamed ML file file | diff | annotate
Mon, 03 Feb 2014 15:19:07 +0100 blanchet merged 'reconstructors' and 'proof methods' file | diff | annotate
Mon, 03 Feb 2014 10:14:18 +0100 blanchet made SML/NJ happier file | diff | annotate
Mon, 03 Feb 2014 10:14:18 +0100 blanchet got rid of 'try0' step that is now redundant file | diff | annotate
Sun, 02 Feb 2014 20:53:51 +0100 blanchet rationalized threading of 'metis' arguments file | diff | annotate
Sun, 02 Feb 2014 20:53:51 +0100 blanchet tuning file | diff | annotate
Sun, 02 Feb 2014 20:53:51 +0100 blanchet made SML/NJ happier file | diff | annotate
Fri, 31 Jan 2014 16:10:39 +0100 blanchet tuning file | diff | annotate
Fri, 31 Jan 2014 13:42:47 +0100 blanchet compile file | diff | annotate
Fri, 31 Jan 2014 12:30:54 +0100 blanchet refactor large ML file file | diff | annotate
less more (0) tip
isabelle