Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) outside ac.uk; Tue, 15 Jun 1993 18:44:08 +0100
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA11333;
          Tue, 15 Jun 93 10:18:32 -0700
Sender: info-hol-request@ted.cs.uidaho.edu
Errors-To: info-hol-request@ted.cs.uidaho.edu
Precedence: bulk
Received: from imec.be by ted.cs.uidaho.edu (16.6/1.34) id AA11328;
          Tue, 15 Jun 93 10:18:21 -0700
Received: from imec.imec.be (imec) by imec.be (5.65c/IDA-1.4.4-IMEC) 
          id AA14870d; Tue, 15 Jun 1993 19:18:34 +0200
Date: Tue, 15 Jun 93 19:17:43 +0200
From: Catia Angelo <catia@imec.be>
Message-Id: <9306151717.AA11818@imec.imec.be>
Original-Received: by imec.imec.be Tue, 15 Jun 93 
                   19:17:43 +0200
PP-warning: Illegal Received field on preceding line
To: info-hol@ted.cs.uidaho.edu
Subject: greatest theory in contrib


Hello Hollers,

Two weeks ago I sent a message to info-hol about a theory on
the MAX generalization. This theory has definitions and theorems
about the greatest of a list of natural numbers. It was developed
to reason about inequalities involving the greatest of a list of
natural numbers. Some proof procedures have also been developed.

This stuff is available by FTP as contrib directory "greatest"
and it works under HOL.2.0. However John Harrison just told me that
it fails under HOL.2.01 :-(

I hope it can be useful to somebody.

Catia


Catia Angelo
catia@imec.be