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_problem.ML
Thu, 26 Nov 2020 18:45:19 +0100 desharna proper parsing of type encoding; file | diff | annotate
Thu, 26 Nov 2020 18:06:36 +0100 desharna proper handling of builtins in TFX file | diff | annotate
Thu, 26 Nov 2020 13:47:29 +0100 desharna proper generation of TPTP output for higher order builtins file | diff | annotate
Thu, 19 Nov 2020 15:11:37 +0100 desharna reintroduced and renamed THF_Predicate_Free deleted by c7e2a9bdc585 file | diff | annotate
Thu, 19 Nov 2020 14:43:50 +0100 desharna renamed data type file | diff | annotate
Wed, 18 Nov 2020 13:44:34 +0100 desharna Tuned parentheses in TPTP output file | diff | annotate
Thu, 05 Nov 2020 18:14:02 +0100 desharna Added support for TFX to Sledgehammer file | diff | annotate
Fri, 02 Oct 2020 10:18:50 +0200 desharna Add more tacing to sledgehammer_isar_trace file | diff | annotate
Tue, 22 Jan 2019 17:22:09 +0100 blanchet tune ATP settings file | diff | annotate
Tue, 22 May 2018 17:15:02 +0200 blanchet added lambda-free HO output for Ehoh (higher-order E prototype) file | diff | annotate
Thu, 11 Jan 2018 13:48:17 +0100 wenzelm uniform use of Standard ML op-infix -- eliminated warnings; file | diff | annotate
Wed, 10 Jan 2018 15:25:09 +0100 nipkow ran isabelle update_op on all sources 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, 02 Nov 2015 21:49:49 +0100 blanchet make sure that function types are never generated as '> @ A @ B', but always as 'A > B' file | diff | annotate
Wed, 26 Nov 2014 20:05:34 +0100 wenzelm renamed "pairself" to "apply2", in accordance to @{apply 2}; file | diff | annotate
Mon, 06 Oct 2014 19:19:16 +0200 blanchet get rid of 'individual' type in DFG proofs file | diff | annotate
Thu, 07 Aug 2014 12:17:41 +0200 blanchet put comments between TPTP lines to comply with TPTP BNF file | diff | annotate
Wed, 30 Jul 2014 14:03:12 +0200 fleury imported patch hilbert_choice_support file | diff | annotate
Tue, 24 Jun 2014 12:36:45 +0200 blanchet added parentheses around type arguments in THF 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 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
Sun, 04 May 2014 18:14:58 +0200 blanchet improved whitelist (cf. be1874de8344) file | diff | annotate
Thu, 01 May 2014 09:30:35 +0200 haftmann optional case enforcement file | diff | annotate
Fri, 25 Apr 2014 11:58:10 +0200 blanchet reintroduced '...' (nonexhaustive) syntax for SPASS-Pirate file | diff | annotate
Thu, 19 Dec 2013 19:35:50 +0100 blanchet tuning 'case' expressions file | diff | annotate
Thu, 19 Dec 2013 15:47:17 +0100 blanchet extended ATP types with sorts 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
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
Fri, 07 Jun 2013 22:17:22 -0400 blanchet SPASS has more Uppercase keywords than I was fearing -- better always append _ file | diff | annotate
Mon, 20 May 2013 12:35:29 +0200 blanchet freeze types in Sledgehammer goal, not just terms file | diff | annotate
Mon, 20 May 2013 11:49:56 +0200 blanchet generate agsyHOL-friendly THF (to some extent -- partial application of connectives remains an issue) file | diff | annotate
Mon, 20 May 2013 11:35:55 +0200 blanchet tuned code file | diff | annotate
Thu, 16 May 2013 13:05:52 +0200 blanchet reintroduced syntax for "nonexhaustive" datatypes file | diff | annotate
Thu, 16 May 2013 13:05:52 +0200 blanchet more work on SPASS datatypes file | diff | annotate
Wed, 15 May 2013 18:39:20 +0200 blanchet more work on SPASS datatypes file | diff | annotate
Wed, 15 May 2013 18:09:20 +0200 blanchet tuning file | diff | annotate
Wed, 15 May 2013 18:06:40 +0200 blanchet no need to reinvent the wheel ("fold_map") file | diff | annotate
Wed, 15 May 2013 18:05:46 +0200 blanchet more work on implementing datatype output for new SPASS file | diff | annotate
Wed, 15 May 2013 17:49:39 +0200 blanchet tuned code 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, 15 May 2013 17:27:24 +0200 blanchet added datatype declaration syntax for next-gen SPASS file | diff | annotate
Mon, 06 May 2013 11:03:08 +0200 smolkas handle dummy atp terms file | diff | annotate
Tue, 09 Apr 2013 15:19:14 +0200 blanchet work on CASC LTB ISA exporter file | diff | annotate
Thu, 13 Dec 2012 23:22:10 +0100 blanchet generate original name as a comment in SPASS problems as well file | diff | annotate
Thu, 13 Dec 2012 22:49:08 +0100 blanchet generate comments with original names for debugging 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
Mon, 23 Jul 2012 15:32:30 +0200 blanchet distinguish between recursive and nonrecursive definitions + clean up typedef dependencies in MaSh file | diff | annotate
Tue, 26 Jun 2012 11:14:40 +0200 blanchet renamed experimental option file | diff | annotate
Tue, 26 Jun 2012 11:14:40 +0200 blanchet finished implementation of DFG type class output file | diff | annotate
Tue, 26 Jun 2012 11:14:40 +0200 blanchet more work on DFG type classes file | diff | annotate
Tue, 26 Jun 2012 11:14:40 +0200 blanchet more work on class support file | diff | annotate
Tue, 26 Jun 2012 11:14:40 +0200 blanchet generate type classes for polymorphic DFG format (SPASS) file | diff | annotate
Tue, 26 Jun 2012 11:14:40 +0200 blanchet cleanly distinguish between type declarations and symbol declarations file | diff | annotate
Tue, 26 Jun 2012 11:14:40 +0200 blanchet added sorts to datastructure file | diff | annotate
Tue, 26 Jun 2012 11:14:40 +0200 blanchet implement polymorphic DFG output, without type classes for now file | diff | annotate
Tue, 26 Jun 2012 11:14:39 +0200 blanchet added type arguments to "ATerm" constructor -- but don't use them yet file | diff | annotate
Tue, 26 Jun 2012 11:14:39 +0200 blanchet started adding polymophic SPASS output file | diff | annotate
less more (0) -100 -60 tip
isabelle