| Mon, 29 Mar 2010 19:49:57 +0200 | blanchet | added "modulus" and "sorts" options to control Sledgehammer's Isar proof output | changeset | files |
| Mon, 29 Mar 2010 18:44:24 +0200 | blanchet | make Sledgehammer output "by" vs. "apply", "qed" vs. "next", and any necessary "prefer" | changeset | files |
| Mon, 29 Mar 2010 15:50:18 +0200 | blanchet | get rid of Polyhash, since it's no longer used | changeset | files |
| Mon, 29 Mar 2010 15:26:19 +0200 | blanchet | remove use of Polyhash; | changeset | files |
| Mon, 29 Mar 2010 14:49:53 +0200 | blanchet | reintroduce efficient set structure to collect "no_atp" theorems | changeset | files |
| Mon, 29 Mar 2010 12:21:51 +0200 | blanchet | made "theory_const" a Sledgehammer option; | changeset | files |
| Mon, 29 Mar 2010 12:01:00 +0200 | blanchet | added "respect_no_atp" and "convergence" options to Sledgehammer; | changeset | files |
| Wed, 31 Mar 2010 16:44:41 +0200 | bulwahn | adding MREC induction rule in Imperative HOL | changeset | files |