Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) outside ac.uk; Tue, 22 Jun 1993 12:27:34 +0100
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA04250;
          Tue, 22 Jun 93 04:17:47 -0700
Sender: info-hol-request@ted.cs.uidaho.edu
Errors-To: info-hol-request@ted.cs.uidaho.edu
Precedence: bulk
Received: from swan.cl.cam.ac.uk by ted.cs.uidaho.edu (16.6/1.34) id AA04245;
          Tue, 22 Jun 93 04:17:40 -0700
Received: from dunlin.cl.cam.ac.uk (user lcp (rfc931)) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) to cl; Tue, 22 Jun 1993 12:17:57 +0100
To: info-hol@ted.cs.uidaho.edu
Subject: HOL90 and ML
Date: Tue, 22 Jun 93 12:17:52 +0100
From: Lawrence C Paulson <Larry.Paulson@cl.cam.ac.uk>
Message-Id: <"swan.cl.cam.:138120:930622111800"@cl.cam.ac.uk>


The pair of books, "The Definition of Standard ML" and "Commentary on Standard
ML", by Milner et al., published by MIT Press, are ML's defining documents. 
Other implementations are more faithful to the Definition than New Jersey is,
and they should hardly be criticised for that.

It is a pity if HOL90 only works with one particular implementation of
Standard ML, since other implementations (notably Poly/ML) are more efficient.

							Larry Paulson