Mercurial Mercurial > repos > isabelle / file revisions
summary | shortlog | changelog | graph | tags | bookmarks | branches | file | revisions | annotate | diff | comparison | rss | help
(0) -300 -100 -60 tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/ATP/atp_systems.ML
Fri, 04 Apr 2014 11:49:47 +0200 blanchet improved parsing of "z3_tptp" proofs file | diff | annotate
Thu, 03 Apr 2014 17:16:02 +0200 blanchet don't pass Vampire option that doesn't exist anymore (and that wasn't strictly necessary with older Vampires) file | diff | annotate
Thu, 03 Apr 2014 17:00:14 +0200 blanchet use Alt-Ergo 0.95.2, the latest and greatest version file | diff | annotate
Thu, 03 Apr 2014 16:57:19 +0200 blanchet updated Z3 TPTP to 4.3.1+ file | diff | annotate
Wed, 18 Dec 2013 16:50:14 +0100 blanchet made SML/NJ happier file | diff | annotate
Tue, 17 Dec 2013 14:03:29 +0100 blanchet primitive support for SPASS-Pirate (Daniel Wand's polymorphic SPASS prototype) file | diff | annotate
Thu, 24 Oct 2013 12:43:33 +0200 blanchet use definitions for LEO-II as well -- this simplifies the code and matches some users' expectations file | diff | annotate
Thu, 12 Sep 2013 22:10:57 +0200 blanchet prefixed types and some functions with "atp_" for disambiguation file | diff | annotate
Wed, 11 Sep 2013 09:50:48 +0200 blanchet adjusted number of generated monomorphic instances for new monomorphizer based on new evaluation (E, SPASS, Vampire) file | diff | annotate
Wed, 28 Aug 2013 18:44:50 +0200 blanchet got rid of old error -- users who install SPASS manually are responsible for any version mismatches file | diff | annotate
Tue, 13 Aug 2013 10:26:56 +0200 blanchet Vampire 3.0 requires types to be declared -- make it happy (and get rid of "implicit" types since only Satallax seems to support them anymore) file | diff | annotate
Mon, 29 Jul 2013 15:30:31 +0200 blanchet added support for E 1.8's internal proof objects (eliminating the need for "eproof_ram") file | diff | annotate
Sun, 26 May 2013 14:02:03 +0200 blanchet 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) file | diff | annotate
Tue, 21 May 2013 09:02:58 +0200 blanchet disabled choice in Satallax file | diff | annotate
Tue, 21 May 2013 09:02:58 +0200 blanchet prefer compiled version of LEO-II and Satallax if available file | diff | annotate
Tue, 21 May 2013 09:02:58 +0200 blanchet updated remote provers file | diff | annotate
Mon, 20 May 2013 11:27:13 +0200 blanchet started adding agsyHOL as an experimental prover file | diff | annotate
Wed, 15 May 2013 17:43:42 +0200 blanchet renamed Sledgehammer functions with 'for' in their names to 'of' file | diff | annotate
Wed, 08 May 2013 15:47:19 +0200 blanchet use right default for "uncurried_aliases" with polymorphic SPASS file | diff | annotate
Fri, 03 May 2013 10:27:24 +0200 blanchet tuning file | diff | annotate
Fri, 03 May 2013 10:26:34 +0200 blanchet pass certain readability-enhancing Vampire options only when an Isar proof is needed file | diff | annotate
Mon, 08 Apr 2013 12:11:06 +0200 blanchet robustness w.r.t. unknown arguments file | diff | annotate
Wed, 20 Mar 2013 15:35:35 +0100 blanchet use the right role for SPASS hypotheses file | diff | annotate
Tue, 05 Mar 2013 11:59:58 +0100 blanchet polymorphic SPASS is also SPASS file | diff | annotate
Thu, 21 Feb 2013 12:22:26 +0100 blanchet swap slices so that the last slice is more complete (for minimization) file | diff | annotate
Wed, 20 Feb 2013 15:26:19 +0100 blanchet upgraded to Alt-Ergo 0.95 file | diff | annotate
Wed, 20 Feb 2013 10:45:01 +0100 blanchet turn off more evil Vampire options to facilitate Isar proof generation file | diff | annotate
Sun, 03 Feb 2013 17:31:33 +0100 blanchet tuned slicing (E-MaLeS and E-Par) file | diff | annotate
Sat, 02 Feb 2013 17:25:55 +0100 blanchet tune slices further file | diff | annotate
Sat, 02 Feb 2013 10:13:14 +0100 blanchet tweak ATP slices further file | diff | annotate
Thu, 31 Jan 2013 17:54:05 +0100 blanchet tuned slices file | diff | annotate
Thu, 31 Jan 2013 17:54:05 +0100 blanchet store fact filter along with ATP slice file | diff | annotate
Thu, 17 Jan 2013 17:55:02 +0100 blanchet make SPASS more configurable, for experiments file | diff | annotate
Thu, 17 Jan 2013 14:01:45 +0100 blanchet added E-Par support file | diff | annotate
Mon, 03 Dec 2012 20:55:32 +0100 blanchet tweak SPASS default a tiny bit, so that a more interesting heuristic is chosen when "slicing=false" (for experiments) file | diff | annotate
Wed, 31 Oct 2012 11:23:21 +0100 blanchet less verbose -- the warning will reach the users anyway by other means file | diff | annotate
Wed, 31 Oct 2012 11:23:21 +0100 blanchet tuned messages file | diff | annotate
Wed, 31 Oct 2012 11:23:21 +0100 blanchet added a timeout around script that relies on the network file | diff | annotate
Wed, 31 Oct 2012 11:23:21 +0100 blanchet tuning file | diff | annotate
Tue, 14 Aug 2012 16:09:45 +0200 blanchet tone down "z3_tptp", now that Z3 (starting with 4.1) no longer supports TPTP TFF0 file | diff | annotate
Tue, 14 Aug 2012 15:23:28 +0200 blanchet tweak Vampire setup in the light of new evaluation file | diff | annotate
Tue, 07 Aug 2012 22:54:27 +0200 blanchet proper quoting file | diff | annotate
Tue, 07 Aug 2012 14:29:18 +0200 blanchet stop distinguishing between complete and incomplete slices, since this is very fragile and has hardly any useful semantics to users file | diff | annotate
Tue, 07 Aug 2012 13:03:50 +0200 blanchet specify full path to clausifier file | diff | annotate
Mon, 06 Aug 2012 22:12:17 +0200 blanchet added iProver(-Eq) local file | diff | annotate
Thu, 02 Aug 2012 10:10:29 +0200 blanchet support older versions of Vampire file | diff | annotate
Thu, 02 Aug 2012 10:10:29 +0200 blanchet added E-MaLeS to list of provers for testing file | diff | annotate
Fri, 27 Jul 2012 17:34:33 +0200 blanchet tweaks in preparation for type encoding evaluation file | diff | annotate
Fri, 27 Jul 2012 08:52:40 +0200 blanchet extract Z3 unsat cores (for "z3_tptp") file | diff | annotate
Fri, 20 Jul 2012 22:19:45 +0200 blanchet use "eproof_ram" script if available (plug-in replacement for "eproof", but faster) file | diff | annotate
Tue, 10 Jul 2012 23:36:03 +0200 blanchet don't ask E to generate a detailed proofs if not needed file | diff | annotate
Tue, 26 Jun 2012 11:14:39 +0200 blanchet started adding polymophic SPASS output file | diff | annotate
Tue, 26 Jun 2012 11:14:39 +0200 blanchet tuning file | diff | annotate
Tue, 26 Jun 2012 11:14:39 +0200 blanchet removed support for unsorted DFG, now that SPASS 3.7 is no longer supported file | diff | annotate
Wed, 06 Jun 2012 10:35:05 +0200 blanchet pass more facts to LEO-II, in the light of latest evaluation file | diff | annotate
Wed, 06 Jun 2012 10:35:05 +0200 blanchet robust LEO-II setup that doesn't rely on ".leoatprc" file | diff | annotate
Wed, 06 Jun 2012 10:35:05 +0200 blanchet tweaked remote Vampire version file | diff | annotate
Mon, 28 May 2012 20:51:23 +0200 blanchet tweaked remote Vampire setup file | diff | annotate
Mon, 28 May 2012 20:45:28 +0200 blanchet killed SPASS 3.5/3.7 FLOTTER hack -- requires users to upgrade to SPASS 3.8 file | diff | annotate
Mon, 28 May 2012 20:25:38 +0200 blanchet don't generate definitions for LEO-II -- this cuases more harm than good file | diff | annotate
less more (0) -300 -100 -60 tip
isabelle