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, 11 Feb 1994 04:01:10 +0000
Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA06182;
          Thu, 10 Feb 1994 19:32:04 -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 AA06178;
          Thu, 10 Feb 1994 19:31:54 -0700
Received: from Maui.CS.UCLA.EDU by dworshak.cs.uidaho.edu 
          with SMTP (1.37.109.8/16.2) id AA22841;
          Thu, 10 Feb 1994 18:30:03 -0800
Received: from LocalHost.cs.ucla.edu 
          by maui.cs.ucla.edu (Sendmail 5.61d+YP/3.23) id AA03960;
          Thu, 10 Feb 94 18:29:57 -0800
Message-Id: <9402110229.AA03960@maui.cs.ucla.edu>
To: info-hol@cs.uidaho.edu
Subject: Dependency graph of theorems
Date: Thu, 10 Feb 94 18:29:55 PST
From: chou@CS.UCLA.EDU

Does anyone one has a program which can read the proof script of
an HOL theory and print out the graph of dependency relations
between theorems?  By "theorems" I mean only those that are
important enough to be proved with "store_thm", "prove", etc.

Thanks in advance!

- Ching Tsun