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 17:40:16 +0100 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA09529; Fri, 9 Apr 93 09:22:02 -0700 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Precedence: bulk Received: from swan.cl.cam.ac.uk by ted.cs.uidaho.edu (16.6/1.34) id AA09524; Fri, 9 Apr 93 09:21:54 -0700 Received: from auk.cl.cam.ac.uk (user jrh (rfc931)) by swan.cl.cam.ac.uk with SMTP (PP-6.4) to cl; Fri, 9 Apr 1993 17:21:15 +0100 To: chou@edu.ucla.cs Cc: info-hol@edu.uidaho.cs.ted (hol mailing list) Subject: Re: How should HOL be pronounced? In-Reply-To: Your message of Fri, 09 Apr 93 00:05:58 -0700. <9304090706.AA18722@maui.cs.ucla.edu> Date: Fri, 09 Apr 93 17:21:08 +0100 From: John Harrison Message-Id: <"swan.cl.ca.442:09.04.93.16.21.29"@cl.cam.ac.uk> I think in Cambridge the favoured pronunciation is "HOL" as in "Holland" (hence "a HOL theory of ..."), though a few mavericks continue to enunciate the letters separately (hence "an H O L theory of ..."). Worldwide, I get the impression that there is about a 50-50 split. Unfortunately, trivial issues like this tend to polarize opinions (cf. "Toposes" vs "Topoi"), so it's probably best not to worry too much about it. John.