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; Fri, 29 Sep 1995 19:08:14 +0100 Received: by leopard.cs.byu.edu (1.37.109.15/16.2) id AA236017039; Fri, 29 Sep 1995 11:50:39 -0600 Sender: info-hol-request@lal.cs.byu.edu Errors-To: info-hol-request@lal.cs.byu.edu Precedence: list Received: from dworshak.cs.uidaho.edu by leopard.cs.byu.edu with ESMTP (1.37.109.15/16.2) id AA235987036; Fri, 29 Sep 1995 11:50:36 -0600 Received: from onyx.dcs.warwick.ac.uk (onyx.dcs.warwick.ac.uk [137.205.224.8]) by dworshak.cs.uidaho.edu (8.6.12/1.1) with ESMTP id KAA05804 for ; Fri, 29 Sep 1995 10:50:17 -0700 Message-Id: <6294.199509291749@onyx.dcs.warwick.ac.uk> Received: from localhost by onyx.dcs.warwick.ac.uk; Fri, 29 Sep 1995 18:49:28 +0100 To: Konrad Slind Cc: shaw@cs.ucdavis.edu, info-hol@cs.uidaho.edu Subject: Re: TRS for HOL90 ? In-Reply-To: Your message of "Fri, 29 Sep 1995 17:40:37 BST." <95Sep29.174038met.8084@sunbroy14.informatik.tu-muenchen.de> Date: Fri, 29 Sep 1995 18:49:27 +0100 From: Sara Kalvala > already contains the "orsml" library. I have used this in some of my > proof efforts and have found it to be useful. The relevant structure has > Alas, one downside to the package is a lamentable lack of documentation. The paper in this year's "H.O.L. and its Applications" workshop (by Elsa Gunter and Leonid Libkin) may be of use for people interested in using the package. Talking of Elsa, I can't resist mentioning the recent birth of her child, apparently named George, at Cambridge. - Sara