Mercurial Mercurial > repos > isabelle / file revisions
summary | shortlog | changelog | graph | tags | bookmarks | branches | file | revisions | annotate | diff | comparison | rss | help
(0) -100 -60 tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/ATP/atp_proof.ML
Fri, 12 Sep 2014 13:27:32 +0200 fleury correction in the thf0 parser ("(=)" found in a Satallax proof). file | diff | annotate
Thu, 28 Aug 2014 23:48:46 +0200 blanchet reworked unskolemization for SPASS file | diff | annotate
Thu, 28 Aug 2014 16:58:27 +0200 blanchet tuned message file | diff | annotate
Mon, 04 Aug 2014 16:55:03 +0200 blanchet tuned comments file | diff | annotate
Mon, 04 Aug 2014 16:53:09 +0200 blanchet deal with E definitions file | diff | annotate
Wed, 30 Jul 2014 14:03:58 +0200 fleury Improving robustness and indentation corrections. file | diff | annotate
Wed, 30 Jul 2014 14:03:13 +0200 fleury Changing the role of rule "tmp_ite_elim" of the SMT solver veriT to Lemma. file | diff | annotate
Wed, 30 Jul 2014 14:03:12 +0200 fleury imported patch hilbert_choice_support file | diff | annotate
Wed, 30 Jul 2014 14:03:12 +0200 fleury imported patch satallax_proof_support_Sledgehammer file | diff | annotate
Mon, 28 Jul 2014 10:57:33 +0200 blanchet correctly translate THF functions from terms to types file | diff | annotate
Thu, 24 Jul 2014 18:46:38 +0200 blanchet filter out 'theory(...)' from dependencies early on file | diff | annotate
Tue, 24 Jun 2014 08:19:57 +0200 blanchet added 'dummy_thf_ml' prover for experiments with HOLyHammer 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:39:41 +0200 blanchet give Z3 TPTP proofs a chance 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:21:39 +0200 fleury Correcting the type parser file | diff | annotate
Mon, 16 Jun 2014 16:18:34 +0200 fleury imported patch leo2_skolem_simplication 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
Wed, 11 Jun 2014 15:29:23 +0200 blanchet moved new highly experimental Waldmeister-specific code (authored by Albert Steckermeier) into Isabelle file | diff | annotate
Tue, 10 Jun 2014 19:15:14 +0200 blanchet tuning file | diff | annotate
Mon, 02 Jun 2014 15:10:18 +0200 fleury basic setup for zipperposition prover file | diff | annotate
Tue, 20 May 2014 16:11:37 +0200 blanchet tuning file | diff | annotate
Fri, 04 Apr 2014 15:56:40 +0200 blanchet use Z3 TPTP cores rather than proofs since the latter are somewhat broken file | diff | annotate
Fri, 04 Apr 2014 11:49:47 +0200 blanchet improved parsing of "z3_tptp" proofs file | diff | annotate
Thu, 30 Jan 2014 20:39:49 +0100 blanchet unskolemize SPASS formula to ensure that the variables are in the right order for 'metis's skolemizer file | diff | annotate
Fri, 20 Dec 2013 14:27:07 +0100 blanchet recognize datatype reasoning in SPASS-Pirate file | diff | annotate
Thu, 19 Dec 2013 15:47:17 +0100 blanchet extended ATP types with sorts file | diff | annotate
Wed, 18 Dec 2013 22:55:20 +0100 blanchet parse SPASS-Pirate types file | diff | annotate
Wed, 18 Dec 2013 17:00:14 +0100 blanchet fixed variable confusion introduced by 'tuning' change 565f9af86d67 file | diff | annotate
Wed, 18 Dec 2013 16:50:14 +0100 blanchet tuning 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
Mon, 16 Dec 2013 23:05:16 +0100 blanchet handle Skolems gracefully for SPASS as well file | diff | annotate
Mon, 16 Dec 2013 17:58:31 +0100 blanchet correcly recognize E skolemization steps that are wrapped in a 'shift_quantors' inference file | diff | annotate
Thu, 12 Sep 2013 23:29:13 +0200 blanchet generalized data structure, for extension with SMT solver proofs 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, 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
Wed, 28 Aug 2013 18:44:50 +0200 blanchet tuned messages file | diff | annotate
Tue, 13 Aug 2013 09:57:55 +0200 blanchet more robust parsing of Vampire proofs with "introduced" names file | diff | annotate
Mon, 29 Jul 2013 16:13:35 +0200 blanchet parse nonnumeric identifiers in E proofs correctly file | diff | annotate
Mon, 29 Jul 2013 15:42:04 +0200 blanchet simplified Vampire hack -- no need to run it for other ATPs file | diff | annotate
Mon, 20 May 2013 13:07:31 +0200 blanchet parse agsyHOL proofs (as unsat cores) file | diff | annotate
Mon, 20 May 2013 11:27:13 +0200 blanchet started adding agsyHOL as an experimental prover file | diff | annotate
Thu, 16 May 2013 13:34:13 +0200 blanchet tuning -- renamed '_from_' to '_of_' in Sledgehammer 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
Mon, 06 May 2013 11:17:33 +0200 smolkas undo 46d911ab9170 since it causes problems file | diff | annotate
Mon, 06 May 2013 11:05:32 +0200 smolkas allow '-'s in tptp ids to avoid problems with remote_vampire file | diff | annotate
Thu, 07 Mar 2013 13:44:54 +0100 blanchet better message (type-unsoundnesses are becoming rare, usually the issue is elsewhere, e.g. in the TSTP proof parser) file | diff | annotate
Wed, 20 Feb 2013 17:31:28 +0100 blanchet generalize syntax of SPASS proofs file | diff | annotate
Wed, 20 Feb 2013 14:21:17 +0100 blanchet tuning (removed redundant datatype) file | diff | annotate
Wed, 20 Feb 2013 10:54:13 +0100 blanchet got rid of rump support for Vampire definitions file | diff | annotate
Thu, 07 Feb 2013 18:39:24 +0100 blanchet more robustness in Isar proof reconstruction (cf. bug report by Ondrej) file | diff | annotate
Thu, 03 Jan 2013 17:10:12 +0100 blanchet rename variable in binder, not just in body file | diff | annotate
Tue, 18 Dec 2012 02:18:45 +0100 blanchet catch all parsing errors file | diff | annotate
Thu, 13 Dec 2012 22:49:08 +0100 blanchet generate comments with original names for debugging file | diff | annotate
Mon, 26 Nov 2012 20:39:19 +0100 wenzelm clarified Symbol.scan_ascii_id; file | diff | annotate
Tue, 06 Nov 2012 11:20:56 +0100 blanchet track formula roles in proofs and use that to determine whether the conjecture should be negated or not file | diff | annotate
Tue, 06 Nov 2012 11:20:56 +0100 blanchet correct parsing of E dependencies 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
Mon, 06 Aug 2012 22:12:17 +0200 blanchet added iProver(-Eq) local file | diff | annotate
Fri, 27 Jul 2012 08:52:40 +0200 blanchet extract Z3 unsat cores (for "z3_tptp") file | diff | annotate
less more (0) -100 -60 tip
isabelle