blanchet [Mon, 29 Mar 2010 19:49:57 +0200] rev 36064
added "modulus" and "sorts" options to control Sledgehammer's Isar proof output
blanchet [Mon, 29 Mar 2010 18:44:24 +0200] rev 36063
make Sledgehammer output "by" vs. "apply", "qed" vs. "next", and any necessary "prefer"
blanchet [Mon, 29 Mar 2010 15:50:18 +0200] rev 36062
get rid of Polyhash, since it's no longer used
blanchet [Mon, 29 Mar 2010 15:26:19 +0200] rev 36061
remove use of Polyhash;
the new code is slightly faster. Also, "subtract_cls" now has canonical argument ordering.
blanchet [Mon, 29 Mar 2010 14:49:53 +0200] rev 36060
reintroduce efficient set structure to collect "no_atp" theorems
blanchet [Mon, 29 Mar 2010 12:21:51 +0200] rev 36059
made "theory_const" a Sledgehammer option;
by default, it's true for SPASS and false for the others. This eliminates the need for the "spass_no_tc" ATP, which can be obtained by passing "no_theory_const" instead.