Three Years of Experience with Sledgehammer, a Practical Link between Automatic and Interactive Theorem Provers.

Lawrence C. Paulson

Browse the full CADE paper archive.