i...@uidaho.edu
-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 ea
Hi Lu,
See the interface at /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 -> un
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 list
