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/TPTP/atp_problem_import.ML
Tue, 10 Feb 2015 14:48:26 +0100 wenzelm proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.; file | diff | annotate
Wed, 26 Nov 2014 20:05:34 +0100 wenzelm renamed "pairself" to "apply2", in accordance to @{apply 2}; file | diff | annotate
Fri, 31 Oct 2014 11:36:41 +0100 wenzelm discontinued obsolete Output.urgent_message; file | diff | annotate
Thu, 07 Aug 2014 12:17:41 +0200 blanchet make TPTP tools work on polymorphic (TFF1) problems as well file | diff | annotate
Thu, 07 Aug 2014 12:17:41 +0200 blanchet treat variables as frees in 'conjecture's file | diff | annotate
Sat, 12 Jul 2014 11:31:23 +0200 blanchet don't generate TPTP THF 'Definition's, because they complicate reconstruction for AgsyHOL and Satallax file | diff | annotate
Mon, 16 Jun 2014 19:44:02 +0200 blanchet compile file | diff | annotate
Mon, 02 Jun 2014 15:10:18 +0200 fleury basic setup for zipperposition prover 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 10:23:32 +0100 blanchet renamed ML file file | diff | annotate
Fri, 31 Jan 2014 10:23:32 +0100 blanchet tuned ML file name file | diff | annotate
Thu, 21 Nov 2013 13:43:42 +0100 blanchet renamed TFF0/THF0 to three-letter acronyms, in keeping with new TPTP policy file | diff | annotate
Mon, 18 Nov 2013 18:04:44 +0100 blanchet send output of "tptp_translate" to standard output, to simplify Geoff Sutcliffe's life file | diff | annotate
Thu, 14 Nov 2013 19:54:10 +0100 blanchet implemented 'tptp_translate' file | diff | annotate
Tue, 30 Jul 2013 15:09:25 +0200 wenzelm type theory is purely value-oriented; file | diff | annotate
Sun, 19 May 2013 20:41:19 +0200 blanchet made "completish" mode a bit more complete file | diff | annotate
Thu, 16 May 2013 13:34:13 +0200 blanchet tuning -- renamed '_from_' to '_of_' in Sledgehammer file | diff | annotate
Thu, 18 Apr 2013 17:07:01 +0200 wenzelm simplifier uses proper Proof.context instead of historic type simpset; file | diff | annotate
Wed, 27 Mar 2013 14:50:30 +0100 wenzelm clarified Skip_Proof.cheat_tac: more standard tactic; file | diff | annotate
Wed, 31 Oct 2012 11:23:21 +0100 blanchet moved Refute to "HOL/Library" to speed up building "Main" even more file | diff | annotate
Wed, 31 Oct 2012 11:23:21 +0100 blanchet use metaquantification when possible in Isar proofs file | diff | annotate
Thu, 16 Aug 2012 15:41:36 +0200 blanchet look in current directory first before looking up includes in the TPTP directory, as required by Geoff file | diff | annotate
Tue, 26 Jun 2012 11:14:40 +0200 blanchet renamed experimental option file | diff | annotate
Wed, 06 Jun 2012 10:35:05 +0200 blanchet add missing timeout multiplier file | diff | annotate
Wed, 06 Jun 2012 10:35:05 +0200 blanchet renamed TPTP commands to agree with Sutcliffe's terminology file | diff | annotate
Wed, 06 Jun 2012 10:35:05 +0200 blanchet don't use aggressive with HO ATP file | diff | annotate
Thu, 24 May 2012 18:21:54 +0200 blanchet make Nitpick's handling of definitions more robust in the face of formulas that don't have the expected format (needed for soundness, cf. RNG100+1) file | diff | annotate
Tue, 22 May 2012 16:59:27 +0200 blanchet compile file | diff | annotate
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" file | diff | annotate
Mon, 30 Apr 2012 21:59:10 +0200 blanchet export more symbols file | diff | annotate
Sun, 29 Apr 2012 11:44:33 +0200 blanchet split into demo and competitive version file | diff | annotate
Fri, 27 Apr 2012 22:36:27 +0200 blanchet use Nitpick as an oracle for finite problems file | diff | annotate
Fri, 27 Apr 2012 22:36:27 +0200 blanchet add extensionality to first-order provers file | diff | annotate
Fri, 27 Apr 2012 15:24:37 +0200 blanchet thread theory cleanly and use "smt" method rather than Sledgehammer for Z3 (because of obscure debilitating bug) file | diff | annotate
Fri, 27 Apr 2012 15:24:37 +0200 blanchet move LEO-II closer to the top, for testing file | diff | annotate
Fri, 27 Apr 2012 15:24:37 +0200 blanchet smaller batches, to play safe file | diff | annotate
Fri, 27 Apr 2012 13:19:21 +0200 blanchet tuning file | diff | annotate
Fri, 27 Apr 2012 12:16:10 +0200 blanchet more tweaking of TPTP/CASC setup file | diff | annotate
Thu, 26 Apr 2012 01:05:06 +0200 blanchet further tweaking for Satallax, so that TPTP problems before parsing and after generation are as similar as possible/practical file | diff | annotate
Thu, 26 Apr 2012 00:28:06 +0200 blanchet tuning; no need for relevance filter file | diff | annotate
Wed, 25 Apr 2012 22:00:33 +0200 blanchet more work on TPTP Isabelle and Sledgehammer tactics file | diff | annotate
Wed, 25 Apr 2012 22:00:33 +0200 blanchet more work on CASC setup file | diff | annotate
Wed, 25 Apr 2012 14:33:21 +0200 blanchet tweak TPTP Nitpick's output file | diff | annotate
Tue, 24 Apr 2012 09:47:40 +0200 blanchet smoother handling of conjecture, so that its Skolem constants get displayed in countermodels file | diff | annotate
Tue, 24 Apr 2012 09:47:40 +0200 blanchet handle TPTP definitions as definitions in Nitpick rather than as axioms file | diff | annotate
Tue, 24 Apr 2012 09:47:40 +0200 blanchet get rid of old parser, hopefully for good file | diff | annotate
Sun, 22 Apr 2012 14:16:46 +0200 blanchet added timeout argument to TPTP tools file | diff | annotate
Sat, 21 Apr 2012 11:15:49 +0200 blanchet prepend PWD to relative paths file | diff | annotate
Sat, 21 Apr 2012 11:15:49 +0200 blanchet reintroduced old FOF and CNF parsers, to work around TPTP_Parser failures file | diff | annotate
Wed, 18 Apr 2012 23:13:11 +0200 blanchet remove old TPTP CNF/FOF parser; always use Nik's new parser file | diff | annotate
Wed, 18 Apr 2012 22:40:25 +0200 blanchet tuned SZS status output file | diff | annotate
Wed, 18 Apr 2012 22:16:05 +0200 blanchet started integrating Nik's parser into TPTP command-line tools file | diff | annotate
Mon, 23 Jan 2012 17:40:32 +0100 blanchet implemented "tptp_refute" tool file | diff | annotate
Mon, 23 Jan 2012 17:40:32 +0100 blanchet added problem importer file | diff | annotate
less more (0) tip
isabelle