Wed, 28 Apr 2010 18:11:11 +0200 | blanchet | make sure short theorem names are preferred to composite ones in Sledgehammer; | changeset | files |
Wed, 28 Apr 2010 17:56:07 +0200 | blanchet | properly extract SPASS proof | changeset | files |
Wed, 28 Apr 2010 17:47:30 +0200 | blanchet | try out Vampire 11 and parse its output correctly; | changeset | files |
Fri, 30 Apr 2010 13:47:39 +0200 | krauss | return updated info record after termination proof | changeset | files |
Fri, 30 Apr 2010 18:06:29 +0200 | wenzelm | proper context for rule_by_tactic; | changeset | files |
Fri, 30 Apr 2010 17:18:29 +0200 | wenzelm | conditional warnings: explicitly observe context visibility flag, not just accidental presence of a context; | changeset | files |