Verbalization of High-Level Formal Proofs

A new approach to text generation from formal proofs that exploits the high-level and interactive features of a tactic-style theorem prover is proposed.