Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) outside ac.uk; Sun, 19 Mar 1995 12:21:29 +0000
Received: by leopard.cs.byu.edu (1.37.109.15/16.2) id AA251454693;
          Sun, 19 Mar 1995 05:04:53 -0700
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: list
Received: from maui.cs.ucla.edu by leopard.cs.byu.edu 
          with SMTP (1.37.109.15/16.2) id AA251424687;
          Sun, 19 Mar 1995 05:04:47 -0700
Received: from LocalHost.cs.ucla.edu by maui.cs.ucla.edu (Sendmail 4.1/3.27) 
          id AA18595; Sun, 19 Mar 95 04:03:16 PST
Message-Id: <9503191203.AA18595@maui.cs.ucla.edu>
To: info-hol@leopard.cs.byu.edu
Subject: Ordinals in HOL?
Date: Sun, 19 Mar 95 04:03:15 PST
From: chou@cs.ucla.edu


Can one have ordinals in HOL (in particular, the ability to do
transfinite recursive definitions and transfinite inductive proofs)?
If so, has anyone done it?

Another question: Which recursive type package allows one to
define the following type?

  ('a,'b)ttt ::= A('a) | B('b -> ttt)

Thanks in advance!

- Ching Tsun