Mon, 20 May 2013 13:07:31 +0200 | blanchet | parse agsyHOL proofs (as unsat cores) | changeset | files |
Mon, 20 May 2013 12:35:29 +0200 | blanchet | freeze types in Sledgehammer goal, not just terms | changeset | files |
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 |