[isabelle] from thy to latex

How to obtain a tex file from a thy file ?

Under JEdit, I have tried "Plugins>Code2HTML>Latex current buffer" but the tex file obtained contains many definitions of the same commands.

courriel : michel.levy2009 at laposte.net
membres-liglab.imag.fr/michel.levy <http://membres-liglab.imag.fr/michel.levy>

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