Return-Path: <john.harrison-request@uk.ac.cam.cl>
Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.0) 
          id <14210-0@swan.cl.cam.ac.uk>; Wed, 10 Jun 1992 22:01:25 +0100
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA04685;
          Wed, 10 Jun 92 13:48:24 -0700
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Received: from Maui.CS.UCLA.EDU by ted.cs.uidaho.edu (16.6/1.34) id AA04679;
          Wed, 10 Jun 92 13:48:16 -0700
Received: from LocalHost.cs.ucla.edu 
          by maui.cs.ucla.edu (Sendmail 5.61b+YP/3.13) id AA05549;
          Wed, 10 Jun 92 13:48:53 -0700
Message-Id: <9206102048.AA05549@maui.cs.ucla.edu>
To: info-hol@edu.uidaho.cs.ted
Cc: chou@edu.ucla.cs
Subject: UNDIRECTED graph theory in HOL?
Date: Wed, 10 Jun 92 13:48:52 PDT
From: chou@edu.ucla.cs

Has anyone developed in HOL a theory of UNDIRECTED graphs?  
I have the graph theory of Dr. Wai Wong, which was presented in last 
year's HOL workshop.  But it seems tailored to directed graphs.

I'd appreciate any pointers!

- Ching Tsun