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; Mon, 6 Mar 1995 09:49:38 +0000
Received: by leopard.cs.byu.edu (1.37.109.15/16.2) id AA163851777;
          Mon, 6 Mar 1995 02:22:57 -0700
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
Received: from TWNMOE10.Edu.TW by leopard.cs.byu.edu 
          with SMTP (1.37.109.15/16.2) id AA163821770;
          Mon, 6 Mar 1995 02:22:50 -0700
Received: from Ruby.ee.nsysu.edu.tw by TWNMOE10.Edu.TW (IBM VM SMTP V2R2) 
          with TCP; Mon, 06 Mar 95 17:14:57 GMT
Date: Mon, 6 Mar 95 17:17:16 CST
From: cclai@Ruby.ee.nsysu.edu.tw (Chi-Chia Lai)
Message-Id: <9503060917.AA03843@Ruby.ee.nsysu.edu.tw>
To: info-hol@leopard.cs.byu.edu
Subject: abstract data type in Isabelle

Hi, everybody:

   I am new to Isabelle. Therefore ,I would like to find if I can define a
   abstract data type in Isabelle???
   It seems that the HOL system[Gordon] can support the definition of
   abstract data type.(we can know this from the paper "A simple Graph
   Theory and Its Application in Railway Signalling"[Wai Wong,1992,IEEE].
   I think most of you should know the paper I mentioned. It is a good
   reference in the field of "HOL verification",isn't it?

   I expect your help.  Thank you very much.

Cheers,
                                                 Chi-Chia Lai