Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Date: Fri, 17 Jan 92 10:45:11 GMT
Message-Id: <9201171045.AA26757@esat.kuleuven.ac.be>
Original-Received: by esat.kuleuven.ac.be Fri,
                   17 Jan 92 10:45:13 GMT
PP-warning: Illegal Received field on preceding line
From: ploegaer@be.imec
To: info-hol@edu.uidaho.cs.ted
Subject: "What's out there?" questions


Strange .. have the impression that my original reply did not get
through ... another trial ...

>>> "Steve"  writes:

        Steve> Here are some questions on what people have already written
        Steve> in terms of automatic packages and how much of it I can get
        Steve> hold of.

I have some kind of an automatic package for proving the equality
of integer expressions in "zet". I ported the old code of this library
(and its parent theories) to hol v.2.00. First "rough" version of the
documentation is finished.
-> expressions = variables and constants and +,- and *

        Steve> First, what about the team from IMEC in the HOL 1991
        Steve> workshop that wrote a package that provided a convenient
        Steve> form of recursion in well-founded structures?  Is it
        Steve> available?  Is it related to the new HOL90 "ind_def"
        Steve> library?

-1- It is not related to the ind_def library

-2- It will be available in the (very) near future. I'm currently
writing the Makefile and the documentation. (well, re-writing such
that it can be used/read by anybody else but myself). A rewrote the
original code completely, such that it is not "utterly slow" anymore.
Any candidates for beta-testing (well, alpha-beta in fact)?

Wim


----------------------------------------------------------------------
Ploegaerts Wim                                e-mail: ploegaer@imec.be
Imec vzw.                                     Tel.:   (32) 16/281 525
Kapeldreef 75                                 Fax.:   (32) 16/281 515
3001   Leuven,  Belgium                       Telex:  26.152