Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) outside ac.uk; Wed, 14 Dec 1994 08:26:57 +0000
Received: by leopard.cs.byu.edu (1.38.193.4/16.2) id AA02968;
          Wed, 14 Dec 1994 01:15:25 -0700
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
Received: from Maui.CS.UCLA.EDU by leopard.cs.byu.edu 
          with SMTP (1.38.193.4/16.2) id AA02963;
          Wed, 14 Dec 1994 01:15:24 -0700
Received: from LocalHost.cs.ucla.edu by maui.cs.ucla.edu (Sendmail 4.1/3.27) 
          id AA16653; Wed, 14 Dec 94 00:10:50 PST
Message-Id: <9412140810.AA16653@maui.cs.ucla.edu>
To: info-hol@leopard.cs.byu.edu
Subject: WANTED: LaTeX environment for HOL formulas
Date: Wed, 14 Dec 94 00:10:49 PST
From: chou@cs.ucla.edu


Is there a LaTeX environment for HOL formulas that is almost idential
to \begin{verbatim} ... \end{verbatim} except that certain special
sequences of characters (eg, !, ?, /\) will be printed in math fonts
(eg, \forall, \exists, \wedge)?  Also, it should preserve the width
of those special sequences of characters (eg, \forall should be in
a box 1-character wide and \wedge in a box 2-character wide).
It would be even nicer if the user can introduce his or her own
special sequences (eg, the user can tell the environment that
~> should be printed using \leadsto).

I'd appreciate any pointers!

- Ching Tsun