Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.4) outside ac.uk; Fri, 9 Apr 1993 08:42:15 +0100 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA08529; Fri, 9 Apr 93 00:06:51 -0700 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Precedence: bulk Received: from Maui.CS.UCLA.EDU by ted.cs.uidaho.edu (16.6/1.34) id AA08523; Fri, 9 Apr 93 00:06:22 -0700 Received: from LocalHost.cs.ucla.edu by maui.cs.ucla.edu (Sendmail 5.61d+YP/3.21) id AA18722; Fri, 9 Apr 93 00:06:03 -0700 Message-Id: <9304090706.AA18722@maui.cs.ucla.edu> To: info-hol@edu.uidaho.cs.ted (hol mailing list) Subject: How should HOL be pronounced? Date: Fri, 09 Apr 93 00:05:58 PDT From: chou@edu.ucla.cs I'm writing a paper entitled "An HOL theory of ..." and so begin wondering how "HOL" should be pronounced. I myself pronounce it as H-O-L, hence I used "an" instead of "a". But I also heard people pronounce it as "hole" or "hall" or "ha-l". I wonder which is more common. - Ching Tsun