| Sun, 01 May 2011 18:37:24 +0200 |
blanchet |
reintroduced constructor for formulas, and automatically detect which logic to use (TFF or FOF) to avoid clutter
|
changeset |
files
|
| Sun, 01 May 2011 18:37:24 +0200 |
blanchet |
added room for types in ATP quantifiers
|
changeset |
files
|
| Sun, 01 May 2011 18:37:24 +0200 |
blanchet |
distinguish FOF and TFF (typed first-order) in ATP abstract syntax tree
|
changeset |
files
|
| Sun, 01 May 2011 18:37:24 +0200 |
blanchet |
remove experimental feature ("risky overload")
|
changeset |
files
|
| Sun, 01 May 2011 18:37:24 +0200 |
blanchet |
added (without implementation yet) new type encodings for Sledgehammer/ATP
|
changeset |
files
|
| Sun, 01 May 2011 18:37:23 +0200 |
blanchet |
close ATP formulas universally earlier, so that we can add type predicates
|
changeset |
files
|
| Sun, 01 May 2011 18:37:23 +0200 |
blanchet |
get rid of "explicit_forall" prover-specific option, even if that means some clutter -- foralls will be necessary to attach types to variables
|
changeset |
files
|
| Sun, 01 May 2011 18:37:23 +0200 |
blanchet |
renamings
|
changeset |
files
|
| Sun, 01 May 2011 18:05:09 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Sun, 01 May 2011 17:55:29 +0200 |
wenzelm |
include static rail files for old manuals, to make standard make job independent of the "rail" executable;
|
changeset |
files
|
| Sun, 01 May 2011 17:42:21 +0200 |
wenzelm |
simplified keyword markup (without formal checking);
|
changeset |
files
|
| Sun, 01 May 2011 17:41:49 +0200 |
wenzelm |
treat @ as separate keyword;
|
changeset |
files
|