Robust, Semi-Intelligible Isabelle Proofs from ATP Proofs. - Steffen Juilf Smolka; Jasmin Christian Blanchette (PxTP@CADE, 2013)

Semi-intelligible Isar Proofs from Machine-Generated Proofs. - Jasmin Christian Blanchette; Sascha Böhme; Mathias Fleury; Steffen Juilf Smolka; Albert Steckermeier (J. Autom. Reason., 2016)