I want to use isabelle build -D xxx
to produce a LaTeX .tex
file out of an Isabelle .thy
file.
But Isabelle checks all the theory dependencies, and all the related .thy
files must be involved.
Is it possible that I casually use a .thy
file that has syntax errors to produce a .tex
file? In fact I only need a part of it to write a paper.
Does that mean you want to write a paper based on a faulty or incomplete formal theory?
The Isabelle document preparation system was intended to publish formal theories that actually work out, with nice typography so that this does not look like "code". So all the defaults are for producing LaTeX from well-formed and checked theories.
Nonetheless, there are numerous ways to get unofficial LaTeX output from the system. A very basic mechanism is the latex
print mode. Various diagnostic commands of Isabelle allow such print mode specifications in round parentheses, e.g. like this:
thm (latex) exI exE
or
print_statement (latex) exI exE
You can do this interactively and copy-paste the output into your raw tex file. You need to ensure that it gets proper surroundings with environments from the isabelle.sty
file.
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With