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 -> unit
val print_theory_as_tex : string -> unit
val print_theories_as_tex_doc : string list -> string -> unit
val tex_theory : string -> unit
You will need the .sty files from thatdirectory (holtex.sty and
holtexbasic.sty). I am not sure if there is more extensive
documentation available yet, but the above is pretty simple
to use.
Konrad.
On Jan 4, 2009, at 4:30 AM, Lu Zhao wrote:
> 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
> [email protected]
> https://lists.sourceforge.net/lists/listinfo/hol-info
------------------------------------------------------------------------------
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
