added "modulus" and "sorts" options to control Sledgehammer's Isar proof output

make Sledgehammer output "by" vs. "apply", "qed" vs. "next", and any necessary "prefer"

get rid of Polyhash, since it's no longer used

remove use of Polyhash; the new code is slightly faster. Also, "subtract_cls" now has canonical argument ordering.

reintroduce efficient set structure to collect "no_atp" theorems

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.

added "respect_no_atp" and "convergence" options to Sledgehammer; these were previously hard-coded in "sledgehammer_fact_filter.ML"

adding MREC induction rule in Imperative HOL

made smlnj happy

adding examples of function predicate replacement and arithmetic examples for the predicate compiler; tuned

adopting specialisation examples to moving the alternative defs in the library

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

no specialisation for predicates without introduction rules in the predicate compiler

improving lookup function to handle overloaded constants more correctly in the function flattening of the predicate compiler