| Mon, 20 May 2013 11:49:56 +0200 | blanchet | generate agsyHOL-friendly THF (to some extent -- partial application of connectives remains an issue) | changeset | files |
| Mon, 20 May 2013 11:35:55 +0200 | blanchet | tuned code | changeset | files |
| Mon, 20 May 2013 11:27:13 +0200 | blanchet | started adding agsyHOL as an experimental prover | changeset | files |
| Mon, 20 May 2013 03:41:58 +0200 | nipkow | defined lvars and rvars of commands separately. | changeset | files |