Return-Path: <john.harrison-request@uk.ac.cam.cl>
Delivery-Date: 
Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.2);
          Wed, 16 Sep 1992 13:12:26 +0100
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA05954;
          Wed, 16 Sep 92 05:03:30 -0700
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
Received: from swan.cl.cam.ac.uk by ted.cs.uidaho.edu (16.6/1.34) id AA05949;
          Wed, 16 Sep 92 05:03:20 -0700
Received: from guillemot.cl.cam.ac.uk (user tfm) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.2) to cl; Wed, 16 Sep 1992 12:52:28 +0100
To: gavan@za.ac.uct.mth.elc (Gavan Tredoux)
Cc: info-hol@edu.uidaho.cs.ted, Tom.Melham@uk.ac.cam.cl
Subject: Re: Ordinals and well founded sets
In-Reply-To: Your message of Mon, 14 Sep 92 19:03:03 +0700. <9209141703.AA01107@elc.mth.uct.ac.za>
Date: Wed, 16 Sep 92 04:38:45 +0100
From: Tom Melham <Tom.Melham@uk.ac.cam.cl>
Message-Id: <"swan.cl.ca.014:16.08.92.11.53.09"@cl.cam.ac.uk>


> Does anyone have a theory of ordinals and/or well-founded
> sets available for reuse? This may be of general interest.

In version 2.0, the contrib directory

   hol/contrib/v11_lib/WELL_ORDER

may be relevant. An updated version of this material will be
avilable in the Library of HOL version 2.01.  Attached is the
READ-ME file for this library.

Tom

%============================================================================%
% LIBRARY:     wellorder                                                     %
%                                                                            %
% DESCRIPTION: Versions of the Axiom of Choice: maximal principles and the   %
%              well-ordering theorem.                                        %
%                                                                            %
% AUTHOR:      John Harrison                                                 %
%              University of Cambridge Computer Laboratory                   %
%              New Museums Site                                              %
%              Pembroke Street                                               %
%              Cambridge CB2 3QG                                             %
%              England.                                                      %
%                                                                            %
%              jrh@cl.cam.ac.uk                                              %
%                                                                            %
% DATE:        30th May 1992                                                 %
%============================================================================%

This library is intended to supersede an earlier library of the same name
written by Ton Kalker, which stopped working in HOL version 1.12. Its format
and the structure of the proofs is somewhat different, providing three maximal
principles: Kuratowski's Lemma, Hausdorff's Maximal Principle and Zorn's Lemma,
en route to the Well-Ordering Theorem.

For full documentation, see "Manual/wellorder.dvi".