Stream: Isabelle/ML

Topic: Generating proof outlines

Szymon Antoniak (Dec 10 2021 at 13:53):

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?

Mathias Fleury (Dec 10 2021 at 14:06):

• 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.

Last updated: Jul 15 2022 at 23:21 UTC