Keyword:Sledgehammer

Papers
Oracle Integration of Floating-Point Solvers with Isabelle Olle Torstensson and Tjark Weber EasyChair Preprint no. 8640
Redirecting Proofs by Contradiction Jasmin Christian Blanchette In:PxTP 2013. Third International Workshop on Proof Exchange for Theorem Proving
Robust, Semi-Intelligible Isabelle Proofs from ATP Proofs Steffen Juilf Smolka and Jasmin Christian Blanchette In:PxTP 2013. Third International Workshop on Proof Exchange for Theorem Proving