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

@inproceedings{DBLP:conf/itp/BinderLK26,
  author       = {Sage Binder and
                  Hanna Lachnitt and
                  Katherine Kosaian},
  editor       = {Ekaterina Komendantskaya and
                  Tobias Nipkow},
  title        = {Apply2Isar: Automatically Converting Isabelle/HOL Apply-Style Proofs
                  to Structured Isar},
  booktitle    = {17th International Conference on Interactive Theorem Proving, {ITP}
                  2026, Lisbon, Portugal, July 26-29, 2026},
  series       = {LIPIcs},
  volume       = {382},
  pages        = {18:1--18:20},
  publisher    = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
  year         = {2026},
  url          = {https://doi.org/10.4230/LIPIcs.ITP.2026.18},
  doi          = {10.4230/LIPICS.ITP.2026.18},
  timestamp    = {Sat, 12 Sep 2026 15:32:53 +0200},
  biburl       = {https://dblp.org/rec/conf/itp/BinderLK26.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}