[isabelle] Build LaTex document without proof checking



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





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.