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; Mon, 4 Sep 1995 15:14:51 +0100 Received: by leopard.cs.byu.edu (1.37.109.15/16.2) id AA134501731; Mon, 4 Sep 1995 07:35:31 -0600 Sender: info-hol-request@lal.cs.byu.edu Errors-To: info-hol-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 AA134211638; Mon, 4 Sep 1995 07:33:58 -0600 Received: from sunbroy14.informatik.tu-muenchen.de ([131.159.0.114]) by tuminfo2.informatik.tu-muenchen.de with SMTP id <26533-4>; Mon, 4 Sep 1995 15:13:28 +0200 Received: by sunbroy14.informatik.tu-muenchen.de id <8087>; Mon, 4 Sep 1995 15:13:21 +0200 From: Konrad Slind To: info-hol@leopard.cs.byu.edu, thomas@nessi.first.gmd.de Subject: hol90 version of Z? Message-Id: <95Sep4.151321met_dst.8087@sunbroy14.informatik.tu-muenchen.de> Date: Mon, 4 Sep 1995 15:13:17 +0200 From comp.specification.z, > From: thomas@nessi.first.gmd.de (Thomas Neustupny) > Newsgroups: comp.specification.z > Subject: Z-Embedding in HOL90 as in HOL88/Contrib ??? > Message-ID: <7315@bigfoot.first.gmd.de> > Date: 4 Sep 95 07:16:22 GMT > Sender: news@bigfoot.first.gmd.de > Lines: 9 > > Hello, > > does anybody know if there exists a free Z embedding in HOL90, > as it exists in the contrib area of HOL88 ? > > Thanks, > Thomas N. Hi Thomas, I am pretty sure that the answer is "no", since the hol88 implementation by Mike Gordon required some extensions to the hol88 parser. Plus, there was a lot of programming in the datatype of preterms. And the prettyprinter had to be changed as well, I think. This work could be paralleled in hol90, by likewise extending the hol90 parser to Z constructs and doing the necessary preterm programming, since the current working version of hol90 makes the preterm type available to users. Konrad.