Return-Path:
Return-Path: <john.harrison-request@uk.ac.cam.cl>
Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP) to cl
          id <24800-0@swan.cl.cam.ac.uk>; Mon, 9 Sep 1991 22:50:28 +0100
Received: from iris.eecs.ucdavis.edu by ted.cs.uidaho.edu (15.11/1.34)
          id AA17802; Mon, 9 Sep 91 14:42:22 pdt
Received: by iris.eecs.ucdavis.edu (5.57/UCD.EECS.7.0) id AA14690;
          Mon, 9 Sep 91 14:43:03 -0700
Received: from localhost by bonzai.cs.ucdavis.edu (4.0/3.15) id AA03163;
          Mon, 9 Sep 91 14:43:02 PDT
Message-Id: <9109092143.AA03163@bonzai.cs.ucdavis.edu>
To: info-hol@edu.uidaho.cs.ted
Subject: PM: Proof Manager
Date: Mon, 09 Sep 91 14:43:01 -0700
From: George Fink <gfink@edu.ucdavis.eecs.bonzai>


The PM Proof Manager system, the visual interface for HOL built in GNU emacs
I reported on in the 1991 HOL Workship here in Davis, is ready for Beta-testing
and is robust enough for general use.  The source and documentation is
available by anonymous ftp at cs.uidaho.edu in the file /pub/hol/pm.tar.Z.

PM works by mapping a backward proof-tree onto a text-based tree display
where subgoals are indented from the parent goal.  Many commands have been
implemented which make the proof process easier to deal with.  See the
documentation for more details.

Refer any questions or comments on PM to me, gfink@cs.ucdavis.edu, I hope
you enjoy using this fine tool.

--George