Received: from finabo.abo.fi (finabo.abo.fi [130.232.17.1]) by ra.abo.fi (8.6.10/8.6.10) with ESMTP id OAA08192; Wed, 15 Nov 1995 14:50:09 +0200 Received: from leopard.cs.byu.edu ("port 1783"@leopard.cs.byu.edu) by finabo.abo.fi (PMDF V5.0-5 #14197) id <01HXOCGZJOLC90OM5J@finabo.abo.fi>; Wed, 15 Nov 1995 14:50:24 +0200 (EET) Received: by leopard.cs.byu.edu (1.37.109.15/16.2) id AA135685143; Wed, 15 Nov 1995 04:32:23 -0700 Received: from swan.cl.cam.ac.uk by leopard.cs.byu.edu with ESMTP (1.37.109.15/16.2) id AA135655140; Wed, 15 Nov 1995 04:32:20 -0700 Received: from puffin.cl.cam.ac.uk (user elg21 (rfc931)) by swan.cl.cam.ac.uk with SMTP (PP-6.5) to cl; Wed, 15 Nov 1995 11:31:36 +0000 Received: by puffin.cl.cam.ac.uk (4.1/SMI-3.0DEV3) id AA07670; Wed, 15 Nov 1995 11:31:16 +0000 (GMT) Date: Wed, 15 Nov 1995 11:31:16 +0000 (GMT) From: Elsa Gunter Subject: Re: Paper available: Representing Datatypes in Isabelle/HOL In-reply-to: <9508251017.AA18438@MAJESTIX.fernuni-hagen.de> (info-hol-request@leopard.cs.byu.edu) Sender: info-hol-request@leopard.cs.byu.edu To: info-hol@leopard.cs.byu.edu Errors-to: info-hol-request@leopard.cs.byu.edu Message-id: <9511151131.AA07670@puffin.cl.cam.ac.uk> MIME-version: 1.0 Content-type: TEXT/PLAIN; CHARSET=US-ASCII Content-transfer-encoding: 7BIT Precedence: list Dear Norbert, Datatypes of the kind you mentioned have been handled for a couple of years by the HOL90 contrib library nested_rec. The underlying principle was discussed briefly at the end of my HUG93 paper. I have been out of commission (and really will continue to be for some time) so I have not had the opportunity of looking at your paper. ---Elsa L. Gunter AT&T Bell Labs elsa@research.att.com