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, 30 Aug 1995 22:22:06 +0100
Received: by leopard.cs.byu.edu (1.37.109.15/16.2) id AA225456602;
          Wed, 30 Aug 1995 15:03:22 -0600
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: list
Received: by leopard.cs.byu.edu (1.37.109.15/16.2) id AA225416602;
          Wed, 30 Aug 1995 15:03:22 -0600
From: Clark Barrett <barrett@lal.cs.byu.edu>
Subject: Changing hol parser
To: info-hol@leopard.cs.byu.edu
Date: Wed, 30 Aug 1995 15:03:21 MDT
X-Mailer: Elm [revision: 109.14]
Message-ID: <"swan.cl.cam.:221020:950830212254"@cl.cam.ac.uk>


I am using Harrison's int package and would like to modify the HOL
parser so that numerical constants are parsed as type :int instead of
type :num.  Is is sufficient to redefine the lisp function "constp",
or is it more complicated than that.

I tried to redefine constp at the top level (after hol and the int
theory had been loaded) and while numbers were parsed as :int,
everything else seemed broken.

If anyone can make some suggestions, I would appreciate it.

-Clark Barrett
barrett@lal.cs.byu.edu