Re: [isabelle] LaTeX document
Francisco Jose CHAVES ALONSO wrote:
I need the TeX file generated by Isabelle, to extract some parts for
another document that I also generate with another command.
"isatool make" delete the TeX generated file. It is possible to save it?
in the IsaMakefile generated by isatool mkdir, there is a line of the form
USEDIR = $(ISATOOL) usedir -v true -i true -d pdf ## -D generated
If you remove the comment sign "##" before "-D generated", isatool make will
save the generated TeX files in the subdirectory MyTheories/generated, where
MyTheories is the subdirectory in which your theory files reside. You can
also replace "-d pdf" by "-d false" if you do not want isatool make to generate
a *.pdf file from the generated TeX files, e.g. because you want to generate
the *.pdf file yourself (after some postprocessing).
Dr. Stefan Berghofer E-Mail: berghofe at in.tum.de
Institut fuer Informatik Phone: +49 89 289 17328
Technische Universitaet Muenchen Fax: +49 89 289 17307
Boltzmannstr. 3 Room: 01.11.059
85748 Garching, GERMANY http://www.in.tum.de/~berghofe
This archive was generated by a fusion of
Pipermail (Mailman edition) and