From ff1ce2b2d7aba6ddd2a0c79e80dd620a11510fa6 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Wed, 8 Mar 2000 06:09:56 +0000
Subject: Elaborated idea a bit

---
 html/projects/thybrowse.html | 14 ++++++++------
 1 file changed, 8 insertions(+), 6 deletions(-)

diff --git a/html/projects/thybrowse.html b/html/projects/thybrowse.html
index bb081fc0..8993d942 100644
--- a/html/projects/thybrowse.html
+++ b/html/projects/thybrowse.html
@@ -5,12 +5,11 @@ theorems and definitions during a proof.  It has notion of displaying
 a "current context" for a proof, and configuration with a proof
 engine command for searching for theorems.  It would be useful to
 extend these facilities with a <i>theory browser</i> for investigating
-the theories currently defined in a running proof assistant.  This
-involves designing a small protocol to communicate with the proof
-assistant and a generic way of displaying theories which have
-different aspects from system to system.  A way which would
-fit in well with Emacs would be to use a <tt>dired</tt>-like
-buffer.
+the theories currently defined in (or available from) a running proof
+assistant.  This involves designing a small protocol to communicate
+with the proof assistant and a generic way of displaying theories
+which have different aspects from system to system.  A way which would
+fit in well with Emacs would be to use a <tt>dired</tt>-like buffer.
 </p>
 <p>
 An alternative version of this project would be to write a standalone
@@ -21,6 +20,9 @@ Java, or in a functional language, Perl, C or C++, so long as a nice
 toolkit is chosen (Qt or GTK).
 </p>
 <p>
+(For a related idea, see the browser integrated with OCaml).
+</p>
+<p>
 <b>Skills:</b>
 Interface programming skills.
 Basic understanding of what theories are for several different proof
-- 
cgit v1.2.3