Return-Path: Delivery-Date: Received: from dworshak.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Thu, 26 Aug 1993 07:36:49 +0100 Received: by dworshak.cs.uidaho.edu (1.37.109.4/16.2) id AA03429; Wed, 25 Aug 93 23:28:00 -0700 Sender: info-hol-request@cs.uidaho.edu Errors-To: info-hol-request@cs.uidaho.edu Precedence: bulk Received: from iraun1.ira.uka.de by dworshak.cs.uidaho.edu with SMTP (1.37.109.4/16.2) id AA03425; Wed, 25 Aug 93 23:27:54 -0700 Received: from ira.uka.de by iraun1.ira.uka.de with SMTP (PP) id <25354-0@iraun1.ira.uka.de>; Thu, 26 Aug 1993 08:27:29 +0200 Date: Thu, 26 Aug 93 8:29:45 MET DST From: reetz To: info-hol@dworshak.cs.uidaho.edu Cc: John.Harrison@cl.cam.ac.uk Subject: RE: HOL improvement survey Message-Id: <"iraun1.ira.358:26.07.93.06.27.31"@ira.uka.de> John Harrison wrote: > As promised at the Vancouver meeting, I'm organizing a survey to > collect views on how the HOL system should be improved. Regarding the bunch of reactions we got about ``num_CONV and pretty printer and...'', it is a topic of interest to add an arithmetic library in the way it was discussed in info-HOL, I think. As I myself see it, it might be in some sense something like the coming word-library. (*****************************************************************************) (* *) (* Ralf Reetz SFB 358 of the german research society (DFG) *) (* reetz@ira.uka.de University of Karlsruhe, Germany *) (* *) (* "we prove around in a ring and suppose, *) (* the goal sits right in the middle and knows." *) (* *) (*****************************************************************************)