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; Tue, 28 Dec 1993 12:12:09 +0000
Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA12207;
          Tue, 28 Dec 1993 05:00:54 -0700
Sender: info-hol-request@leopard.cs.byu.edu
Errors-To: info-hol-request@leopard.cs.byu.edu
Precedence: bulk
Received: from dworshak.cs.uidaho.edu by leopard.cs.byu.edu 
          with SMTP (1.37.109.8/16.2) id AA12203;
          Tue, 28 Dec 1993 05:00:54 -0700
Received: from id.dth.dk by dworshak.cs.uidaho.edu with SMTP (1.37.109.8/16.2) 
          id AA26197; Tue, 28 Dec 1993 03:58:42 -0800
Received: from idcad7.id.dth.dk by iddth.id.dth.dk (5.65c+/1.34) id AA19917;
          Tue, 28 Dec 1993 12:57:02 +0100
Received: by idcad7.id.dth.dk (5.57/1.34) id AA14610;
          Tue, 28 Dec 93 12:57:37 +0100
Date: Tue, 28 Dec 93 12:57:37 +0100
From: Ole Steen Rasmussen (Ph.d.) <osr@id.dth.dk>
Message-Id: <9312281157.AA14610@idcad7.id.dth.dk>
To: info-hol@cs.uidaho.edu
Subject: Dependent types


Hello all 

Has anyone used dependent types and/or subtypes in hol90. 

Thanks.

Ole Rasmussen