> We need people to play with sledgehammer > (anybody doing big proofs at TUM just now?) and to suggest what settings > to provide. Currently I envisage selection of prover and full proofs. > Possibly tweaks to the relevance filter (to tighten or loosen it) may be > useful.
Any guinea-pigs? Sledgehammer will be in the upcoming release, so a little testing can't hurt. I am quite fond of it since it proved i div k = 0 <-> k=0 | 0 <= i < k | k < i <= 0 for me. Tobias
