Blanchette, J. C., Kaliszyk, C., Paulson, L. C., & Urban, J. (2016). Hammering towards QED. Journal of Formalized Reasoning, 9(1), 101–148. https://doi.org/10.6092/issn.1972-5787/4593