| Tue, 24 Jun 2014 12:35:43 +0200 | blanchet | tweaked experimental setup | changeset | files |
| Tue, 24 Jun 2014 08:20:00 +0200 | blanchet | changed order of facts so that 'name_tabs' has the same order everywhere (which affects unaliasing) | changeset | files |
| Tue, 24 Jun 2014 08:19:58 +0200 | blanchet | use strings to communicate with external process, to ease debugging | changeset | files |
| Tue, 24 Jun 2014 08:19:57 +0200 | blanchet | added 'dummy_thf_ml' prover for experiments with HOLyHammer | changeset | files |
| Tue, 24 Jun 2014 08:19:56 +0200 | blanchet | phantoms may also occur in THF1 | changeset | files |
| Tue, 24 Jun 2014 08:19:55 +0200 | blanchet | added experimental MaSh engine | changeset | files |
| Tue, 24 Jun 2014 08:19:55 +0200 | blanchet | move method silencing code closer to the methods it is trying to silence, to reduce bad side-effects | changeset | files |
| Tue, 24 Jun 2014 08:19:54 +0200 | blanchet | help reconstruction of Z3 skolemization by weakening formulas a bit | changeset | files |