Return-Path: Delivery-Date: Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Fri, 25 Aug 1995 13:51:31 +0100 Received: by leopard.cs.byu.edu (1.37.109.15/16.2) id AA080734485; Fri, 25 Aug 1995 06:41:25 -0600 Sender: hol2000-request@lal.cs.byu.edu Errors-To: hol2000-request@lal.cs.byu.edu Precedence: list Received: from swan.cl.cam.ac.uk by leopard.cs.byu.edu with ESMTP (1.37.109.15/16.2) id AA080694466; Fri, 25 Aug 1995 06:41:06 -0600 Received: from albatross.cl.cam.ac.uk (user drs1004 (rfc931)) by swan.cl.cam.ac.uk with SMTP (PP-6.5) to cl; Fri, 25 Aug 1995 13:22:58 +0100 X-Mailer: exmh version 1.6.1 5/23/95 To: hol2000@leopard.cs.byu.edu Subject: Re: Discussion on meta-language for HOL In-Reply-To: Your message of "Fri, 25 Aug 1995 12:58:03 BST." <"swan.cl.cam.:250290:950825115808"@cl.cam.ac.uk> Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii Date: Fri, 25 Aug 1995 13:22:55 +0100 From: Donald Syme Message-Id: <"swan.cl.cam.:261330:950825122301"@cl.cam.ac.uk> > BTW, perhaps Andy Gordon could give us the run down on whether > Miranda would be practical to use for a theorem prover?? Sorry, of course I meant Haskell. All these lazy languages sound the same to me... Don