Apply2Isar: Automatically Converting Isabelle/HOL Apply-Style Proofs to Structured Isar.

Sage Binder, Hanna Lachnitt, Katherine Kosaian

Browse the full ITP paper archive.