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; Fri, 25 Aug 1995 12:03:04 +0100
Received: by leopard.cs.byu.edu (1.37.109.15/16.2) id AA076385740;
          Fri, 25 Aug 1995 04:15:40 -0600
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: list
Received: from ilex.FernUni-Hagen.de by leopard.cs.byu.edu 
          with ESMTP (1.37.109.15/16.2) id AA076355720;
          Fri, 25 Aug 1995 04:15:20 -0600
Received: from MAJESTIX.fernuni-hagen.de by ilex.FernUni-Hagen.de 
          with SMTP (PP); Fri, 25 Aug 1995 12:16:51 +0200
Received: from TRANSFIX.fernuni-hagen.de 
          by MAJESTIX.fernuni-hagen.de (4.1/SMI-4.1) id AA18438;
          Fri, 25 Aug 95 12:17:07 +0200
Date: Fri, 25 Aug 95 12:17:07 +0200
From: Norbert.Voelker@FernUni-Hagen.de (Norbert Voelker)
Message-Id: <9508251017.AA18438@MAJESTIX.fernuni-hagen.de>
To: info-hol@leopard.cs.byu.edu
Subject: Paper available: Representing Datatypes in Isabelle/HOL

I have written down some remarks about representing datatypes in higher order
logic.  It focuses on the representation of datatypes with recursive
occurences inside other datatypes such as

  'a tree =  Node ('a, 'a tree list)

It is available under the www page of the coming Isabelle workshop

  http://www.cl.cam.ac.uk/users/lcp/Workshop/index.html

As usual, comments are very welcome. 

--Norbert Voelker