[isabelle-dev] Sledgehammer

[Tobias Nipkow]

> 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