Fri, 01 Aug 2014 19:32:46 +0200 |
blanchet |
no need to 'obtain' variables not in formula
|
changeset |
files
|
Fri, 01 Aug 2014 19:32:10 +0200 |
blanchet |
more precise handling of LEO-II skolemization
|
changeset |
files
|
Fri, 01 Aug 2014 16:07:34 +0200 |
blanchet |
beware of 'skolem' rules that do not skolemize (e.g. LEO-II)
|
changeset |
files
|
Fri, 01 Aug 2014 16:07:33 +0200 |
blanchet |
tuning
|
changeset |
files
|
Fri, 01 Aug 2014 16:07:33 +0200 |
blanchet |
peek instead of joining -- is perhaps less risky
|
changeset |
files
|
Fri, 01 Aug 2014 14:43:57 +0200 |
blanchet |
export ML function
|
changeset |
files
|
Fri, 01 Aug 2014 14:43:57 +0200 |
blanchet |
compile
|
changeset |
files
|
Fri, 01 Aug 2014 14:43:57 +0200 |
blanchet |
removed 'metisFT' support in Mirabelle
|
changeset |
files
|
Fri, 01 Aug 2014 14:43:57 +0200 |
blanchet |
removed Mirabelle minimization code
|
changeset |
files
|
Fri, 01 Aug 2014 14:43:57 +0200 |
blanchet |
modernized Mirabelle (a bit) and made it compile
|
changeset |
files
|
Fri, 01 Aug 2014 14:43:57 +0200 |
blanchet |
restored a bit of laziness
|
changeset |
files
|
Fri, 01 Aug 2014 14:43:57 +0200 |
blanchet |
reorder quantifiers to ease Z3 skolemization
|
changeset |
files
|
Fri, 01 Aug 2014 14:43:57 +0200 |
blanchet |
tuned order of arguments
|
changeset |
files
|
Fri, 01 Aug 2014 14:43:57 +0200 |
blanchet |
tuned name context code
|
changeset |
files
|
Fri, 01 Aug 2014 14:43:57 +0200 |
blanchet |
tuned whitespace
|
changeset |
files
|