Hi, When I use EmitTeX.print_theories_as_tex_doc to export theories into TeX documents, if the target TeX files already exist, the command reports HOL_ERR:
File ../papers/references already exists.
Exception-
HOL_ERR
{message = "File exists", origin_function = "failwith",
origin_structure = "??"} raised
This doesn’t make any sense, I think, as other commands like DB.html_theory ()
does allow overwriting files.
Is there any hidden option that allows me to call
EmitTeX.print_theories_as_tex_doc without deleting existing files first?
Regards,
Chun Tian
signature.asc
Description: Message signed with OpenPGP using GPGMail
------------------------------------------------------------------------------ Check out the vibrant tech community on one of the world's most engaging tech sites, Slashdot.org! http://sdm.link/slashdot
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
