Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Build LaTex document without proof checking

Email Gateway (Aug 18 2022 at 19:51):

From: "C. Diekmann" <diekmann@in.tum.de>
Hello,

I am creating a pdf document from my isabelle theory, using 'isabelle
make -B' to rebuild the pdf document. Unfortunately, this takes very
long. Is it possible (during development) to disable the proof
checking? Most of my text in the .thy files is enclosed in text { *}
blocks. I make heavy use of 'thm' to refer to the definitions.
Unfortunately using 'usedir -D' and working on the generated *.tex files
is not an option. It would be great to see how changes in the *.thy file
end up in the resulting pdf.

Best Regards
Cornelius Diekmann

Last updated: Nov 21 2024 at 12:39 UTC