| Fri, 10 Sep 2010 15:36:49 +0200 |
wenzelm |
removed spurious addition from 9e58f0499f57;
|
changeset |
files
|
| Fri, 10 Sep 2010 15:17:44 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Fri, 10 Sep 2010 14:37:57 +0200 |
krauss |
improved error message for common mistake (fun f where "g x = ...")
|
changeset |
files
|
| Fri, 10 Sep 2010 10:59:10 +0200 |
bulwahn |
adding another String.literal example
|
changeset |
files
|
| Fri, 10 Sep 2010 10:59:09 +0200 |
bulwahn |
fiddling with the correct setup for String.literal
|
changeset |
files
|
| Fri, 10 Sep 2010 10:59:07 +0200 |
bulwahn |
refactoring mode inference so that the theory is not changed in the mode inference procedure
|
changeset |
files
|
| Fri, 10 Sep 2010 10:21:25 +0200 |
haftmann |
Haskell == is infix, not infixl
|
changeset |
files
|
| Fri, 10 Sep 2010 09:56:28 +0200 |
haftmann |
more correct dependencies
|
changeset |
files
|
| Thu, 09 Sep 2010 20:58:46 +0200 |
blanchet |
merged
|
changeset |
files
|
| Thu, 09 Sep 2010 20:11:52 +0200 |
blanchet |
use definitional CNF for the goal if at least one of the premisses would lead to too many clauses in Meson
|
changeset |
files
|
| Thu, 09 Sep 2010 20:09:43 +0200 |
blanchet |
use the Meson cutoff as the cutoff for using definitional CNF -- it's simpler that way
|
changeset |
files
|
| Thu, 09 Sep 2010 18:53:55 +0200 |
blanchet |
clarify comment
|
changeset |
files
|
| Thu, 09 Sep 2010 18:50:23 +0200 |
blanchet |
improve on 65903ec4e8e8: fix more "add_ffpair" exceptions in failed ATP proofs
|
changeset |
files
|
| Thu, 09 Sep 2010 18:22:04 +0200 |
blanchet |
allow Sledgehammer proofs containing nameless local facts with schematic variables in them
|
changeset |
files
|
| Thu, 09 Sep 2010 16:32:28 +0200 |
blanchet |
tuning
|
changeset |
files
|