Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.2); Tue, 15 Sep 1992 10:14:56 +0100 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA03023; Tue, 15 Sep 92 02:02:12 -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 AA03018; Tue, 15 Sep 92 02:02:04 -0700 Received: from dunlin.cl.cam.ac.uk (user lcp) by swan.cl.cam.ac.uk with SMTP (PP-6.2) to cl; Tue, 15 Sep 1992 09:59:57 +0100 To: info-hol@edu.uidaho.cs.ted Subject: Ordinals and well founded sets Date: Tue, 15 Sep 92 09:58:47 +0100 From: Lawrence Paulson Message-Id: <"swan.cl.ca.483:15.08.92.09.00.44"@cl.cam.ac.uk> Isabelle-92 provides an implementation of ZF set theory including ordinals, well-founded recursion and transfinite recursion. Ordinal arithmetic has not been defined, but this could easily be done by transfinite recursion. Larry Paulson