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, 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
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
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
Wed, 23 May 2012 21:19:48 +0200 blanchet tuned names file | diff | annotate
Sun, 13 May 2012 16:31:01 +0200 blanchet extend ATP data structure to avoid having to perform ((non-)capture avoiding) beta reduction -- fixes a bug in the THF translation of "is_measure.simps" file | diff | annotate
Wed, 25 Apr 2012 22:00:33 +0200 blanchet don't use the native choice operator if the type encoding isn't higher-order file | diff | annotate
Tue, 27 Mar 2012 16:59:13 +0300 blanchet tuning (in particular, Symtab instead of AList) file | diff | annotate
Tue, 27 Mar 2012 16:59:13 +0300 blanchet be less forceful about ":lt" to make infinite loops less likely (could still fail with mutually recursive tail rec functions) file | diff | annotate
Tue, 27 Mar 2012 16:59:13 +0300 blanchet avoid DL file | diff | annotate
Wed, 21 Mar 2012 16:53:24 +0100 blanchet generate weights and precedences for predicates as well file | diff | annotate
Tue, 20 Mar 2012 18:42:45 +0100 blanchet removed obsolete temporary hack file | diff | annotate
Tue, 20 Mar 2012 18:42:45 +0100 blanchet tweaks file | diff | annotate
Tue, 20 Mar 2012 10:45:52 +0100 blanchet don't generate new SPASS constructs for old SPASS file | diff | annotate
Tue, 20 Mar 2012 00:44:30 +0100 blanchet continued implementation of term ordering attributes file | diff | annotate
Tue, 20 Mar 2012 00:44:30 +0100 blanchet internal renamings file | diff | annotate
Fri, 24 Feb 2012 11:23:35 +0100 blanchet added support for Alt-Ergo through Why3 (mostly for experimental purposes, e.g. polymorphism vs. monomorphization) file | diff | annotate
Thu, 09 Feb 2012 14:42:18 +0100 blanchet minor DFG fix file | diff | annotate
Thu, 09 Feb 2012 14:04:17 +0100 blanchet improved KBO weights -- beware of explicit applications file | diff | annotate
Thu, 09 Feb 2012 12:57:59 +0100 blanchet added possibility of generating KBO weights to DFG problems file | diff | annotate
Sat, 04 Feb 2012 12:08:18 +0100 blanchet improved hashing w.r.t. Mirabelle, to help debugging file | diff | annotate
Sat, 04 Feb 2012 12:08:18 +0100 blanchet tuned SPASS DFG output file | diff | annotate
Fri, 03 Feb 2012 18:00:55 +0100 blanchet extended SPASS/DFG output with ranks file | diff | annotate
Thu, 02 Feb 2012 01:55:17 +0100 blanchet tuning file | diff | annotate
Wed, 01 Feb 2012 17:16:55 +0100 blanchet really fixed syntax bug in DFG output (cf. ef62c2fafa9e) file | diff | annotate
Tue, 31 Jan 2012 15:13:18 +0100 blanchet avoid name clash, really file | diff | annotate
Tue, 31 Jan 2012 15:10:03 +0100 blanchet fixed syntax bug in DFG output file | diff | annotate
Tue, 31 Jan 2012 14:39:21 +0100 blanchet new SPASS setup file | diff | annotate
Tue, 31 Jan 2012 12:43:48 +0100 blanchet distinguish between ":lr" and ":lt" (terminating) in DFG format file | diff | annotate
Tue, 31 Jan 2012 10:29:05 +0100 blanchet nicer keyword class avoidance scheme file | diff | annotate
Thu, 26 Jan 2012 20:49:54 +0100 blanchet better handling of individual type for DFG format (SPASS) file | diff | annotate
Mon, 23 Jan 2012 17:40:32 +0100 blanchet renamed two files to make room for a new file file | diff | annotate
Tue, 20 Dec 2011 18:59:50 +0100 blanchet don't try to avoid SPASS keywords; instead, just suffix an underscore to all generated identifiers file | diff | annotate
Tue, 20 Dec 2011 18:59:50 +0100 blanchet one more SPASS identifier file | diff | annotate
Tue, 13 Dec 2011 14:55:42 +0100 blanchet correctly declare implicit TFF1 types that appear first as type arguments with "$tType" and not "$i file | diff | annotate
Sat, 29 Oct 2011 13:15:58 +0200 blanchet always use DFG format to talk to SPASS -- since that's what we'll need to use anyway to benefit from sorts and other extensions file | diff | annotate
less more (0) -100 -60 tip
isabelle