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
bulwahn [Wed, 31 Mar 2010 16:44:41 +0200] rev 36054
adopting specialisation examples to moving the alternative defs in the library
bulwahn [Wed, 31 Mar 2010 16:44:41 +0200] rev 36053
adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn [Wed, 31 Mar 2010 16:44:41 +0200] rev 36052
no specialisation for predicates without introduction rules in the predicate compiler
bulwahn [Wed, 31 Mar 2010 16:44:41 +0200] rev 36051
improving lookup function to handle overloaded constants more correctly in the function flattening of the predicate compiler