Updated.

2 files changed, 185 insertions, 10 deletions

diff --git a/ChangeLog b/ChangeLog
index 058e47f9..d0b411cc 100644
--- a/ChangeLog
+++ b/ChangeLog
@@ -1,3 +1,177 @@
+2002-08-29  David Aspinall  <da@proofgeneral.org>
+
+	* isa/isabelle-system.el:
+	Dependencies classed as experimental.
+
+	* doc/PG-adapting.texi: Update magic
+
+	* etc/announce, etc/release-log.txt:
+	Updated.
+
+	* Makefile:
+	Simplify byte comp, notes of brokenness.
+
+	* etc/announce-header.txt: New files.
+
+	* todo, TODO, isa/README:
+	Updated.
+
+	* isar/isar.el, isa/isa.el:
+	New theorem deps settings
+
+	* phox/example.phx: AF2 eradicate
+
+	* etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el:
+	Set version tag for new release.
+
+	* generic/proof-menu.el:
+	Simplify menu structure further by adding Advanced menu.
+
+	* doc/ProofGeneral.texi: Update magic
+
+	* html/download.html, html/news.html, html/oldnews.html:
+	News about 3.4; links to download.
+
+	* plastic/plastic.el:
+	Fix calls on proof-defshortcut
+
+2002-08-28  David Aspinall  <da@proofgeneral.org>
+
+	* plastic/plastic.el:
+	Fix interactive posn
+
+	* generic/proof-menu.el:
+	Comments: possible fix to compiles.
+
+	* generic/proof-menu.el:
+	Fix for docstrings in proof-def-shortcut, proof-def-invisible.
+
+	* generic/proof-utils.el:
+	Alternative version of proof-ass macro to support byte-compiled files.
+
+	* generic/proof-script.el:
+	checkdoc induced docstring tweaks.
+
+	* generic/proof-depends.el:
+	Change to proof-shell-theorem-dependency-regexp; also add code to make nested submenus of deps.
+
+	* generic/proof-shell.el, generic/proof-config.el:
+	Change proof-shell-theorem-dependency-regexp to use two pieces: names and dependencies
+
+	* etc/isar/Fibonacci.thy:
+	Borrowed as example
+
+	* generic/proof-compat.el:
+	Compatibility fixes from Stefan Monnier.
+
+	* isa/isabelle-system.el:
+	Add missing semicolon.
+
+	* isa/depends.ML: Deleted file
+
+	* coq/coq-syntax.el:
+	Patch from Stefan Monnier for syntax highlighting.
+
+	* doc/localdir, doc/PG-adapting.texi, doc/ProofGeneral.texi:
+	Update dir entries, remove localdir file
+
+	* generic/proof-site.el:
+	Patch from Stefan Monnier <monnier+gnu/emacs@rum.cs.yale.edu> for Info config.
+
+	* generic/proof-shell.el, generic/proof-config.el:
+	Add proof-shell-theorem-dependency-list-split
+
+	* generic/proof-utils.el:
+	Docstring/CR from stefans patch
+
+	* generic/proof-script.el:
+	Make font-lock-keywords buffer local for sake of Emacs 21.2.
+
+	* etc/isar/XSymbolTests.thy:
+	Exercise bug in pg-remove-specials breaking x-sym display in Isabelle
+
+	* generic/proof-utils.el:
+	Fix bug in pg-remove-specials breaking x-sym display in Isabelle
+
+	* html/mailinglist:
+	Mention support@proofgeneral.org address.
+
+	* etc/Mailman/intro-proofgeneraldevel.html, etc/Mailman/intro-proofgeneral.html:
+	Update intros.
+
+	* README, FAQ:
+	Contact in case of probs.
+
+	* generic/pg-goals.el, generic/pg-response.el:
+	Make font-lock-keywords buffer local for sake of Emacs 21.2.
+
+	* phox/phox-tags.el:
+	Fix to calls on message
+
+	* generic/proof-splash.el:
+	Disable pop-up-frames for splash.
+
+	* coq/coq.el, generic/proof-toolbar.el:
+	Fix sloppy uses of message/concat
+
+2002-08-27  Markus Wenzel  <wenzelm@informatik.tu-muenchen.de>
+
+	* isa/isabelle-system.el, isa/isa.el, isar/isar.el:
+	proper setup for theorem dependencies;
+
+	* generic/proof-menu.el:
+	proof-assistant-format: always pass through proof-assistant-setting-format;
+
+2002-08-27  David Aspinall  <da@proofgeneral.org>
+
+	* ChangeLog: Updated.
+
+	* etc/ProofGeneral.spec, html/devel.html, generic/proof-site.el, html/develdownload.php:
+	Set version tag for new release.
+
+	* doc/ProofGeneral.texi: Updated magic
+
+	* generic/pg-response.el: Docstring
+
+	* generic/proof-menu.el:
+	Move C-c C-w to universal keys
+
+	* generic/proof-config.el:
+	Add C-c C-w to universal keys.
+
+	* generic/proof-menu.el:
+	Key for pg-response-clear-displays.
+
+	* generic/proof-menu.el: Conventions
+
+	* CHANGES: Updated.
+
+	* etc/announce: Updated
+
+	* doc/dir, doc/localdir:
+	Tweak
+
+	* doc/dir: Add PG adapting.
+
+	* generic/proof-config.el: Menu name
+
+	* BUGS: Updated.
+
+	* generic/proof-shell.el:
+	Disable undo history for efficiency; improve kill buffer hook.
+
+	* generic/proof-menu.el:
+	Menu entry to clear response buffers.
+
+	* generic/pg-response.el:
+	Disable undo history for efficiency; add clear response buffers function; clear modified flag.
+
+	* generic/pg-goals.el:
+	Disable undo history for efficiency.
+
+	* README.devel, README:
+	Updated
+
 2002-08-27  David Aspinall  <da@proofgeneral.org>
 
 	* etc/ProofGeneral.spec, html/devel.html, generic/proof-site.el, html/develdownload.php:
diff --git a/README.exper b/README.exper
index 3424863d..2b6c718c 100644
--- a/README.exper
+++ b/README.exper
@@ -28,24 +28,25 @@ Current "experimental" features
    in orange.   This allows easy editing of theories to remove
    dead lemmas, re-order proofs, etc.
 
-   Only works for Isabelle/classic at the moment (support is
-   required from proof assistant authors: please mention to them).  
-   You must select the Isabelle option "Theorem Dependencies",
-   and then restart Isabelle.
+   This only works for a pre-release version of Isabelle at the moment.
+   (Support is required from other proof assistant authors: please 
+   mention to them).  You must select the Isabelle setting 
+   "Theorem Dependencies".
 
 ** Active highlighting for variables in Isabelle.
    Moving the mouse over variables in the goal display will display
    some information.  The information in Isabelle/Isar is the type of
-   the variable, usually.  In Isabelle it is useless.
-   This feature is a hint of what could be done with proper subterm
+   the variable, often, but it depends on the context and may be
+   wrong.  In Isabelle/classic the type information is useless.
+   This feature is a vague hint of what could be done with proper subterm
    markup from the Isabelle engine.  Without this, it cannot work
-   well, because no context is available to Proof General, so only
-   variables bound at the outer level can have meaningful information
-   displayed, via the "term" command.
+   well, because no context is available for Proof General to send
+   back to the prover, so only variables bound at the outer level can 
+   have sensible information displayed, via the "term" command.
 
 
 Known problems with experimental features
 =========================================
 
-** Move up/down functions make spoil visibility behaviour.
+** Move up/down functions may spoil visibility behaviour.
    
\ No newline at end of file