diff options
| author | David Aspinall | 2001-08-31 20:08:19 +0000 |
|---|---|---|
| committer | David Aspinall | 2001-08-31 20:08:19 +0000 |
| commit | 88eaaf397c81def616192308955e6e94af24e96c (patch) | |
| tree | b5010c3c8f75b463712865f4d5b27657cf05755a /doc | |
| parent | b3de9663905e9fa254bf49473b6e8067bb11ae9a (diff) | |
Something about dependencies feature
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/ProofGeneral.texi | 17 |
1 files changed, 12 insertions, 5 deletions
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. |