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.
blanchet [Mon, 29 Mar 2010 12:01:00 +0200] rev 36058
added "respect_no_atp" and "convergence" options to Sledgehammer;
these were previously hard-coded in "sledgehammer_fact_filter.ML"
bulwahn [Wed, 31 Mar 2010 16:44:41 +0200] rev 36057
adding MREC induction rule in Imperative HOL
bulwahn [Wed, 31 Mar 2010 16:44:41 +0200] rev 36056
made smlnj happy
bulwahn [Wed, 31 Mar 2010 16:44:41 +0200] rev 36055
adding examples of function predicate replacement and arithmetic examples for the predicate compiler; tuned