| Thu, 10 May 2012 16:56:23 +0200 |
blanchet |
distinguish between instantiated and uninstantiated inductions -- the latter are OK for first-order provers
|
file |
diff |
annotate
|
| Thu, 26 Apr 2012 00:33:23 +0200 |
blanchet |
tuning
|
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
|
| Wed, 21 Mar 2012 16:53:24 +0100 |
blanchet |
generate weights and precedences for predicates as well
|
file |
diff |
annotate
|
| Mon, 19 Mar 2012 21:10:33 +0100 |
wenzelm |
moved some legacy stuff;
|
file |
diff |
annotate
|
| Sat, 17 Mar 2012 09:51:18 +0100 |
wenzelm |
'definition' no longer exports the foundational "raw_def";
|
file |
diff |
annotate
|
| Tue, 28 Feb 2012 15:54:51 +0100 |
blanchet |
speed up Sledgehammer's clasimpset lookup a bit
|
file |
diff |
annotate
|
| Wed, 08 Feb 2012 00:05:22 +0100 |
blanchet |
beware of "Bit0" and "Bit1" -- these shouldn't be blidly unfolded by SPASS, lest we get gigantic terms
|
file |
diff |
annotate
|
| Thu, 02 Feb 2012 01:55:17 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Wed, 01 Feb 2012 12:47:43 +0100 |
blanchet |
proper statuses for "fact_from_ref"
|
file |
diff |
annotate
|
| Tue, 31 Jan 2012 12:43:48 +0100 |
blanchet |
distinguish between ":lr" and ":lt" (terminating) in DFG format
|
file |
diff |
annotate
|
| Thu, 26 Jan 2012 20:49:54 +0100 |
blanchet |
even more lr tags for SPASS -- anything that is considered an "equational rule spec" is relevant
|
file |
diff |
annotate
|
| Thu, 26 Jan 2012 20:49:54 +0100 |
blanchet |
separate orthogonal components
|
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
|
| Sat, 14 Jan 2012 19:06:05 +0100 |
wenzelm |
renamed Term.all to Logic.all_const, in accordance to HOLogic.all_const;
|
file |
diff |
annotate
|
| Mon, 02 Jan 2012 14:32:20 +0100 |
blanchet |
removed special handling for set constants in relevance filter
|
file |
diff |
annotate
|
| Sat, 24 Dec 2011 16:14:58 +0100 |
haftmann |
dropped references to obsolete facts `mem_def` and `Collect_def`
|
file |
diff |
annotate
|
| Sat, 29 Oct 2011 13:15:58 +0200 |
blanchet |
added sorted DFG output for coming version of SPASS
|
file |
diff |
annotate
|
| Wed, 21 Sep 2011 15:55:15 +0200 |
blanchet |
tuned comment
|
file |
diff |
annotate
|
| Thu, 15 Sep 2011 10:57:40 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Wed, 07 Sep 2011 13:50:17 +0200 |
blanchet |
parse new experimental '@' encodings
|
file |
diff |
annotate
|
| Wed, 07 Sep 2011 13:50:17 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Wed, 31 Aug 2011 11:52:03 +0200 |
blanchet |
more tuning
|
file |
diff |
annotate
|
| Tue, 30 Aug 2011 14:12:55 +0200 |
nik |
improved handling of induction rules in Sledgehammer
|
file |
diff |
annotate
|
| Tue, 30 Aug 2011 14:12:55 +0200 |
nik |
added generation of induction rules
|
file |
diff |
annotate
|
| Wed, 24 Aug 2011 11:17:33 +0200 |
blanchet |
more reliable "sledgehammer\_tac" reconstruction, by avoiding "insert_tac"
|
file |
diff |
annotate
|
| Mon, 22 Aug 2011 15:02:45 +0200 |
blanchet |
removed unused configuration option
|
file |
diff |
annotate
|
| Mon, 27 Jun 2011 22:44:44 +0200 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Mon, 27 Jun 2011 14:56:33 +0200 |
blanchet |
don't export any metastrange or other nonatomizable formulas, since these don't help proving normal things, they are somewhat broken in the ATP output, and they are atypical
|
file |
diff |
annotate
|
| Mon, 27 Jun 2011 15:03:55 +0200 |
wenzelm |
old gensym is now legacy -- global state is out of fashion, and its result is not guaranteed to be fresh;
|
file |
diff |
annotate
|