Fri, 18 Oct 2013 14:58:02 +0200 | blanchet | set code attribute on discriminator equations | changeset | files |
Fri, 18 Oct 2013 13:38:55 +0200 | blanchet | MaSh error handling | changeset | files |
Fri, 18 Oct 2013 13:30:09 +0200 | blanchet | repair invariant in MaSh when learning new proofs | changeset | files |
Fri, 18 Oct 2013 10:43:21 +0200 | blanchet | killed more "no_atp"s | changeset | files |
Fri, 18 Oct 2013 10:43:20 +0200 | blanchet | killed most "no_atp", to make Sledgehammer more complete | changeset | files |
Fri, 18 Oct 2013 10:35:57 +0200 | blanchet | doc fixes suggested by Andreas L. | changeset | files |
Fri, 18 Oct 2013 10:35:56 +0200 | blanchet | make sure that registered code equations are actually equations | changeset | files |
Fri, 18 Oct 2013 10:35:55 +0200 | blanchet | accept very long lines in MaSh | changeset | files |