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; Thu, 4 Mar 1993 09:40:29 +0000 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA17665; Thu, 4 Mar 93 01:29:43 -0800 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 AA17660; Thu, 4 Mar 93 01:29:34 -0800 Received: from teal.cl.cam.ac.uk (user rjb (rfc931)) by swan.cl.cam.ac.uk with SMTP (PP-6.4) to cl; Thu, 4 Mar 1993 09:29:04 +0000 To: toal@edu.ucla.cs (Ray J. Toal) Cc: info-hol@edu.uidaho.cs.ted Subject: Re: arithmetic In-Reply-To: Your message of Wed, 03 Mar 93 17:26:27 -0800. <9303040126.AA25731@makaha.cs.ucla.edu> Date: Thu, 04 Mar 93 09:28:58 +0000 From: Richard Boulton Message-Id: <"swan.cl.ca.642:04.03.93.09.29.07"@cl.cam.ac.uk> > True or False? There is no ARITH_CONV in HOL 2.0. True. You need HOL88 v2.01. Richard.