Apologies if this chat is not meant for questions like this, this is my first question.

Is there a canonical way to generate a proof outline file from a complete thory file (as in https://www.isa-afp.org/browser_info/current/AFP/Concurrent_Ref_Alg/outline.pdf)? If so, is it possible to pick to format of the file (say, txt instead of pdf) and disable Latex typesetting?

- standard way: https://isabelle.in.tum.de/dist/Isabelle2021/doc/system.pdf, chapter 3
- No way to generate a txt, only a PDF, a tex, and the HTML documentation. The TeX is used in particular for snippets https://isabelle.in.tum.de/community/Generate_TeX_Snippets.

Szymon Antoniak has marked this topic as resolved.

Last updated: Sep 11 2024 at 16:22 UTC