From 88eaaf397c81def616192308955e6e94af24e96c Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Fri, 31 Aug 2001 20:08:19 +0000
Subject: Something about dependencies feature

---
 doc/ProofGeneral.texi | 17 ++++++++++++-----
 1 file changed, 12 insertions(+), 5 deletions(-)

(limited to 'doc')

diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi
index d114a962..73e021b2 100644
--- a/doc/ProofGeneral.texi
+++ b/doc/ProofGeneral.texi
@@ -220,13 +220,20 @@ other documentation, system downloads, etc.
 @unnumberedsec Latest news for 3.3
 @cindex news
 
-Proof General 3.3 includes a few small features additions, but mainly
-the focus has been on compatibility improvements for new versions of
-provers (in particular, Coq 7), and new versions of emacs (in
-particular, XEmacs 21.4).
+Proof General 3.3 includes a few feature additions, but mainly the focus
+has been on compatibility improvements for new versions of provers (in
+particular, Coq 7), and new versions of emacs (in particular, XEmacs
+21.4).
 
 One new feature is control over visibility of completed proofs,
-@xref{Visibility of completed proofs}.
+@xref{Visibility of completed proofs}.  Another new feature is the
+tracking of theorem dependencies inside Isabelle.  A context-sensitive
+menu (right-button on proof scripts) provides facility for browsing the
+ancestors and child theorems of a theorem, and highlighting them.  The
+idea of this feature is that it can help you untangle and rearrange big
+proof scripts, by seeing which parts are interdependent.  The implementation
+is provisional and not documented yet in the body of this manual.  It only
+works for the "classic" version of Isabelle99-2.
 
 See the @file{CHANGES} file in the distribution for more complete
 details of changes since 3.2.
-- 
cgit v1.2.3