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; Thu, 24 Aug 1995 17:21:40 +0100 Received: by leopard.cs.byu.edu (1.37.109.15/16.2) id AA017039503; Thu, 24 Aug 1995 09:51:43 -0600 Sender: hol2000-request@lal.cs.byu.edu Errors-To: hol2000-request@lal.cs.byu.edu Precedence: list Received: from tuminfo2.informatik.tu-muenchen.de by leopard.cs.byu.edu with ESMTP (1.37.109.15/16.2) id AA016349345; Thu, 24 Aug 1995 09:49:05 -0600 Received: from sunbroy14.informatik.tu-muenchen.de ([131.159.0.114]) by tuminfo2.informatik.tu-muenchen.de with SMTP id <26503-4>; Thu, 24 Aug 1995 17:50:50 +0200 Received: by sunbroy14.informatik.tu-muenchen.de id <8087>; Thu, 24 Aug 1995 17:50:42 +0200 From: Konrad Slind To: jgrundy@ra.abo.fi Cc: john.harrison@cl.cam.ac.uk, hol2000@leopard.cs.byu.edu In-Reply-To: <199508241342.QAA17185@aton.abo.fi> (message from Jim Grundy INF on Thu, 24 Aug 1995 15:42:18 +0200) Subject: Re: Paper available: "HOL Done Right" Message-Id: <95Aug24.175042met_dst.8087@sunbroy14.informatik.tu-muenchen.de> Date: Thu, 24 Aug 1995 17:50:32 +0200 > Is this possible, or am I dreaming. I think it's possible and desirable. The problem is that John has "a visceral dislike" for the syntax of SML. Having a front end that would present a "Classic-ML"-ish interface to one of these SML systems would probably help a lot of people. But it would be a really irritating and boring piece of software to write. Really, I think that the ML community shot itself in the foot by not finding a "Standard" they could all live with. Konrad.