[Hol-info] convert HOL formula to latex

Hi, I'd like to put some HOL theorems in a paper that is written in latex. Is there an easy way to format HOL formulas nicely in latex? Thanks. Lu -- ___ hol-info mailing

Re: [Hol-info] convert HOL formula to latex

Hi Lu, See the interface at holdir/src/emit/EmitTeX.sig. This allows tex to be generated from HOL terms, definitions, theorems and theories. Snippet: val print_term_as_tex : term - unit val print_type_as_tex : hol_type - unit val print_theorem_as_tex : thm

Re: [Hol-info] convert HOL formula to latex

-Original Message- From: Lu Zhao [mailto:luz...@cs.utah.edu] Sent: Sunday, January 04, 2009 3:30 AM To: hol-info@lists.sourceforge.net Subject: [Hol-info] convert HOL formula to latex Hi, I'd like to put some HOL theorems in a paper that is written in latex. Is there an easy way to format HOL