| 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 |