Re: [isabelle] LaTeX document



Francisco Jose CHAVES ALONSO wrote:
Hi,

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?

Hello Francisco,

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

Greetings,
Stefan

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