There is a really old interface (search for latex) on the archive:
http://www.cl.cam.ac.uk/research/hvg/FTP/FTP.html
I have attached the files.
I put this together for HOL 90 (I haven't used HOL in many years). It was a
set of LaTeX macros to process a snippet of HOL 90 code and "pretty print
it".
If you can not find anything else, maybe you can convert this to something
that works for you
---
Dr. Jim Alves-Foss, Director
Center for Secure and Dependable Systems
University of Idaho
Moscow, ID 83844-1008
em: ji...@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 easy way to format HOL formulas nicely in latex?
Thanks.
Lu
--
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
hol_macros.tex
Description: Binary data
% - %
% DIRECTORY: latex %
% %
% DESCRIPTION: LaTeX macros for typesetting HOL.%
% %
% AUTHOR: Jim Alves-Foss%
% %
% ADDRESS: University of California Davis, %
% Davis, CA 95616, U.S.A. %
% %
% email: f...@iris.eecs.ucdavis.edu%
% %
% DATE: 90.12.14%
% - %
The file hol_macros.tex is a collection of macros developed at UC Davis to be
used in placing HOL code in papers. These macros take the (almost) standard
HOL output and convert it into the LaTeX logic symbols (ie. ! is \forall, ? is
\exists, etc.) This is the BETA VERSION (so check the outputs to be safe).
You should redefine '\' as '\\' by "set_lambda`\\.`;; " so LaTeX does not
get confused (HOL still works fine).
We have the following environments:
\begin{hol} ... \end{hol} Defines an environment for HOL theorems and
definitions. This environment it identical to alltt except
that it places a box around the text and ~ still works
\begin{holnb} ... \end{holnb} Same as ``hol'' but no box
We have the following macros:
\holthm{defn} Which takes defn (cut directly from HOL output
and converts all the symbols (ie. |- ==>) to their
mathematical equivalents.
\holdef{defn} Same as holthm except that the turnstile is subscripted
by ``def''
I hope you can use these, please send me any comments:
-Jim Alves-Foss (f...@iris.eecs.ucdavis.edu) [128.120.57.20]
--
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
