From b3de9663905e9fa254bf49473b6e8067bb11ae9a Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Fri, 31 Aug 2001 20:04:33 +0000 Subject: Added note about dependency feature. --- CHANGES | 27 ++++++++++++++++++++++++++- 1 file changed, 26 insertions(+), 1 deletion(-) diff --git a/CHANGES b/CHANGES index 97b08da1..a67489c6 100644 --- a/CHANGES +++ b/CHANGES @@ -63,7 +63,9 @@ Compatibility for V7 added. Experimental enhancements to handling of compiled files and - file dependency. (Only tested with Coq 6.3.1) + file dependency. (Only tested with Coq 6.3.1: we need help + from Coq implementors to add primitive support in V7, please + appeal to them to help Proof General!). 1) At the end of scripting foo.v (i.e. when activing scripting is switched off), "Reset Initial. Compile Module " is @@ -89,6 +91,29 @@ This functionality is enabled with the Coq settings option "Auto Compile Vos". + +** Isabelle Changes + + Support for theorem dependency tracking: in-context menu provides + facility for browsing the ancestors and child theorems of a + theorem, and highlighting them. This facility is not yet closely + integrated with Isabelle and relies on an auxiliary ML file which + is only compatible with Isabelle99-2. It is only supplied for + Isabelle/classic. + + The idea of this feature is that it can help you untangle and + rearrange big proof scripts, by seeing which parts are + interdependent. + + To activate the feature, use the Isabelle setting option "Theorem + Dependencies." Notice that you need to switch this on *after* + starting an Isabelles session, and must switch on/off on every + restart. (This behaviour will improve once better integrated + with Isabelle). + + Not yet documented. Comments and suggestions welcome. + + ** Changes for developers to note *** proof-shell-process-output now sets proof-shell-last-output and -- cgit v1.2.3