A Computer Environment for Writing Ordinary Mathematical Proofs. - David McMath; Marianna Rozenfeld; Richard Sommer (LPAR, 2001)