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: [email protected] -----Original Message----- From: Lu Zhao [mailto:[email protected]] Sent: Sunday, January 04, 2009 3:30 AM To: [email protected] 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 [email protected] 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: [email protected] % % % % 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 ([email protected]) [128.120.57.20]
------------------------------------------------------------------------------
_______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
