Return-Path: <john.harrison-request@uk.ac.cam.cl>
Delivery-Date: 
Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.0) 
          id <05211-0@swan.cl.cam.ac.uk>; Thu, 9 Jul 1992 08:33:11 +0100
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA07256;
          Thu, 9 Jul 92 00:26:32 -0700
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Received: from Maui.CS.UCLA.EDU by ted.cs.uidaho.edu (16.6/1.34) id AA07251;
          Thu, 9 Jul 92 00:26:28 -0700
Received: from LocalHost.cs.ucla.edu 
          by maui.cs.ucla.edu (Sendmail 5.61c+YP/3.19) id AA16234;
          Thu, 9 Jul 92 00:27:32 -0700
Message-Id: <9207090727.AA16234@maui.cs.ucla.edu>
To: info-hol@edu.uidaho.cs.ted
Subject: Re: What is $# in the HOL logic?
In-Reply-To: Your message of "Wed, 08 Jul 92 23:14:02 BST." <"swan.cl.ca.436:08.06.92.22.14.10"@cl.cam.ac.uk>
Date: Thu, 09 Jul 92 00:27:31 PDT
From: chou@edu.ucla.cs

It seems to me a pretty bad idea to have a hardware-specific device
built into the basic HOL, rather than having it as part of a library.
Not every application of HOL is about hardware.

- Ching Tsun