Fix ChangeLog target so makes prefix properly. Revert to keeping uncompressed file in repo.

1 files changed, 2957 insertions, 0 deletions

diff --git a/ChangeLog b/ChangeLog
new file mode 100644
index 00000000..4a6a1414
--- /dev/null
+++ b/ChangeLog
@@ -0,0 +1,2957 @@
+2000-09-29  David Aspinall  <da@proofgeneral.org>
+
+	* Makefile, Makefile.devel:
+	Add acl2 and twelf to elisp dirs
+
+	* etc/ProofGeneral.spec:
+	Fix adding acl2 and twelf to RPM
+
+	* Makefile.devel:
+	ChangeLog is just last 1000 lines, instead of 11000 starting in 1996...
+
+	* ChangeLog.gz: Updated.
+
+	* html/smallheader.html, html/header.html:
+	Link image to root dir.
+
+	* html/main.html: Tweak
+
+	* etc/ProofGeneral.patch:
+	Remove patch on perl filename now, after Pierres accidental checkin.
+
+	* ChangeLog.gz: Updated.
+
+	* etc/ProofGeneral.spec, html/devel.html, html/develdownload.html, generic/proof-site.el:
+	Set version tag for new release.
+
+	* All files:
+	Updating branch
+
+	* etc/cvs-tips.txt:
+	Note about dealing with backslashname directory.
+
+	* todo: Updated
+
+	* etc/cvs-tips.txt:
+	Note about dealing with backslashname directory.
+
+	* INSTALL:
+	Update URLs and mail aliases.  Mention script, and extensions for new provers
+
+	* bin/proofgeneral:
+	Script for launching proofgeneral.
+
+	* todo: Updated
+
+	* etc/ProofGeneral.spec:
+	Add more provers, and proofgeneral script
+
+	* etc/proofgeneral-domain.txt:
+	Notes about proofgeneral.org
+
+	* images/pgmini.xpm, images/pgicon.png:
+	Add icon images.
+
+	* html/develdownload.html: Minor change
+
+	* INSTALL: Note about packages needed
+
+	* html/functions.php3:
+	Click to go back links to root.
+
+	* html/register.html, html/features.html, html/header.html, html/main.html, html/mission.html, html/oldnews.html, html/projects.html, html/about.html, html/develdownload.html, html/doc.html, html/download.html:
+	Remove messy link_root links.
+
+	* html/links, html/main, html/news, html/about, html/devel, html/doc, html/download, html/features:
+	Short file instead of a link, so works in CVS. Bit annoying to duplicate, but never mind.
+
+	* html/about, html/links, html/devel, html/doc, html/screenshot, html/download, html/features, html/news, html/main:
+	Links for shortcut URLs.
+
+	* html/notes.txt:
+	Mention needed server hacks
+
+	* html/functions.php3:
+	Remove link_root nonsense
+
+	* todo: Updated with fixes before 3.2.
+
+	* BUGS:
+	Inherent problem with Emacs in console mode: no face support
+
+	* Makefile.devel:
+	twelf and acl2 are in ordinary dist
+
+	* etc/announce: Mention ACL2 too
+
+	* twelf/README: Tweak
+
+	* demoisa/demoisa-easy.el: Comment fix
+
+	* generic/proof-script.el:
+	Parse comments also in proof-script-generic-parse-sexp
+
+	* generic/proof-menu.el:
+	Non existent get-window-buffer -> get-buffer-window  (how did that get through?)
+
+	* generic/proof-config.el:
+	Default for proof-comment-end that doesn't cause looping in searching for comment end.
+
+	* acl2/README, acl2/acl2.el, acl2/example.acl2:
+	Updated, trimmed down to barebones.
+
+2000-09-29  Pierre Courtieu  <courtieu@lri.fr>
+
+	* coq/todo:
+	added some comments in coq/todo
+
+2000-09-29  David Aspinall  <da@proofgeneral.org>
+
+	* coq/coqtags, lego/legotags:
+	Make default path to perl be /usr/bin/perl
+
+2000-09-29  Pierre Courtieu  <courtieu@lri.fr>
+
+	* coq/x-symbol-coq.el:
+	a little change in coq/x-symbol, nothing
+
+	* coq/coq.el:
+	A little work around for the bug of Coq concerning the restart that
+	uses Reset Initial which doesn't reset the Implicit Arguments flag to
+	Off (this is the bug), I added the good command to the coq reset
+	command, this has to be backtracked when V7 will be done (the bug is
+	already corrected in V7).
+
+	* lego/legotags, coq/x-symbol-coq.el, coq/coq.el, coq/coqtags, coq/coq-syntax.el:
+	Added Uncaught exception errors in coq-error-regexp.
+
+2000-09-28  David Aspinall  <da@proofgeneral.org>
+
+	* doc/ProofGeneral.texi, doc/PG-adapting.texi:
+	Date becomes Oct
+
+	* acl2/acl2.el: Fix web page, at least.
+
+	* ChangeLog.gz: Updated.
+
+	* twelf/README: Notes.
+
+	* doc/ProofGeneral.texi: Tweaks
+
+	* todo, Makefile.devel:
+	phtml -> html
+
+	* etc/announce: Fix URL.
+
+	* html/download.html, html/index.html:
+	Renamed files
+
+	* phtml -> html
+	Renamed files
+
+	* ChangeLog.gz: Updated.
+
+	* twelf/twelf-font.el: Add FIXME
+
+	* generic/proof-script.el: Fix comment.
+
+	* twelf/twelf.el:
+	Var name change use-new-parsing -> use-new-parser. Turn on font lock by default.
+
+	* doc/ProofGeneral.texi:
+	Fix typo, add credit.
+
+2000-09-28  Markus Wenzel  <wenzelm@informatik.tu-muenchen.de>
+
+	* isar/isar.el: isar-web-page;
+
+2000-09-28  David Aspinall  <da@proofgeneral.org>
+
+	* ChangeLog.gz: Updated.
+
+	* etc/ProofGeneral.spec, html/devel.phtml, html/develdownload.phtml, generic/proof-site.el:
+	Set version tag for new release.
+
+	* doc/Makefile: Add default target
+
+	* acl2/x-symbol-acl2.el, acl2/README, acl2/acl2.el, acl2/example.acl2:
+	First (non-working) versions, committed so that doc builds.
+
+	* README: Fix date
+
+	* README.devel: Dreams about testing
+
+	* todo:
+	Generalize Isabelles atomic file scripting.
+
+	* TODO:
+	Added generic line width adjusting to grand TODO
+
+	* doc/PG-adapting.texi:
+	Added extra section on how to tweak script input to the shell
+
+	* generic/proof-config.el:
+	Added proof-shell-strip-crs-from-input, and unadvertised proof-script-fly-past-comments
+
+	* generic/proof-menu.el:
+	Added fly past comments to quick opts menu when new parsing mechanism active.
+
+	* generic/proof-script.el:
+	Bug fix in proof-goto-end-of-locked.  Comments in new parsing functions.  Tweaks to proof-script-generic-parse-cmdstart.  Combine fly-past and coelesce comment options.  Use proof-string-match-safe in generic-goal-command-p, to avoid error in Twelf.
+
+	* generic/proof-shell.el:
+	Added proof-shell-strip-crs-from-input.
+
+	* twelf/twelf.el, twelf/x-symbol-twelf.el, twelf/example.elf, twelf/twelf-font.el:
+	Fixes to twelf support, begins to work now.
+
+2000-09-28  David Aspinall  <da@proofgeneral.org>
+
+	* doc/ProofGeneral.texi, doc/PG-adapting.texi:
+	Date becomes Oct
+
+	* acl2/acl2.el: Fix web page, at least.
+
+	* ChangeLog.gz: Updated.
+
+	* twelf/README: Notes.
+
+	* doc/ProofGeneral.texi: Tweaks
+
+	* todo, Makefile.devel:
+	phtml -> html
+
+	* etc/announce: Fix URL.
+
+	* html/*.phtml -> *.html  (more)
+	Moved to use .html instead of .phtml
+
+	* html/download.html, html/index.html:
+	Renamed files
+
+	* html/*.phtml -> *.html
+	Renamed files
+
+	* ChangeLog.gz: Updated.
+
+	* twelf/twelf-font.el: Add FIXME
+
+	* generic/proof-script.el: Fix comment.
+
+	* twelf/twelf.el:
+	Var name change use-new-parsing -> use-new-parser. Turn on font lock by default.
+
+	* doc/ProofGeneral.texi:
+	Fix typo, add credit.
+
+2000-09-28  Markus Wenzel  <wenzelm@informatik.tu-muenchen.de>
+
+	* isar/isar.el: isar-web-page;
+
+2000-09-28  David Aspinall  <da@proofgeneral.org>
+
+	* ChangeLog.gz: Updated.
+
+	* etc/ProofGeneral.spec, html/devel.phtml, html/develdownload.phtml, generic/proof-site.el:
+	Set version tag for new release.
+
+	* doc/Makefile: Add default target
+
+	* acl2/x-symbol-acl2.el, acl2/README, acl2/acl2.el, acl2/example.acl2:
+	First (non-working) versions, committed so that doc builds.
+
+	* README: Fix date
+
+	* README.devel: Dreams about testing
+
+	* todo:
+	Generalize Isabelles atomic file scripting.
+
+	* TODO:
+	Added generic line width adjusting to grand TODO
+
+	* doc/PG-adapting.texi:
+	Added extra section on how to tweak script input to the shell
+
+	* generic/proof-config.el:
+	Added proof-shell-strip-crs-from-input, and unadvertised proof-script-fly-past-comments
+
+	* generic/proof-menu.el:
+	Added fly past comments to quick opts menu when new parsing mechanism active.
+
+	* generic/proof-script.el:
+	Bug fix in proof-goto-end-of-locked.  Comments in new parsing functions.  Tweaks to proof-script-generic-parse-cmdstart.  Combine fly-past and coelesce comment options.  Use proof-string-match-safe in generic-goal-command-p, to avoid error in Twelf.
+
+	* generic/proof-shell.el:
+	Added proof-shell-strip-crs-from-input.
+
+	* twelf/twelf.el, twelf/x-symbol-twelf.el, twelf/example.elf, twelf/twelf-font.el:
+	Fixes to twelf support, begins to work now.
+
+2000-09-27  Markus Wenzel  <wenzelm@informatik.tu-muenchen.de>
+
+	* isar/todo:
+	** C func-menu: observe proof-syntactic-context (general problem of
+	func-menu setup?);
+
+	* doc/ProofGeneral.texi:
+	proper spelling: "Leonor Prensa Nieto";
+	fixed @kindex for LEGO and Coq;
+	Isabelle Proof General: cover Isabelle/Isar as well;
+
+	* isar/isar-syntax.el:
+	removed broken outline stuff;
+
+	* isar/isar.el: tuned docstring;
+
+2000-09-27  David Aspinall  <da@proofgeneral.org>
+
+	* etc/ProofGeneral.spec, html/devel.phtml, html/develdownload.phtml, generic/proof-site.el:
+	Set version tag for new release.
+
+	* todo: Updated
+
+	* README: Updated, mention PG Kit.
+
+	* Makefile.devel:
+	proofgeneral email address for me
+
+	* BUGS: Updated
+
+	* doc/PG-adapting.texi:
+	Added future section, fixed URLs.  Updated to mention proof-script-sexp-commands.
+
+	* doc/ProofGeneral.texi:
+	Shortened BUGs appendix, other improvements
+
+	* coq/BUGS: Updated from doc
+
+	* etc/announce: Updated
+
+	* etc/ProofGeneral.spec:
+	Fix URL of source
+
+	* html/images/PG-small.jpg:
+	Already shrunken general for buggy browsers benefit.
+
+	* html/smallheader.phtml, html/mailinglist.phtml, html/main.phtml, html/news.phtml, html/screenshot.phtml, html/doc.phtml, html/feedback.phtml, html/footer.phtml, html/functions.php3, html/header.phtml, html/devel.phtml:
+	Updated web pages, misc improvements.
+
+	* generic/proof-utils.el:
+	Fix bug email address to bugs@proofgeneral.org
+
+	* generic/proof-site.el: Added ACL2
+
+	* generic/proof-config.el, generic/proof-script.el:
+	Added yet another new parsing mechanism, bit more rational this time.
+
+	* isa/BUGS:
+	Added bugs that were mentioned in manual
+
+	* isa/isa.el:
+	Dont use customize-set-variable for add splash logo
+
+	* html/kit.html:
+	Working home page for PG kit
+
+	* html/Kit/dtd/pgip.dtd, html/Kit/dtd/pgml.dtd:
+	Added kit stuff: just copies of the DTDs at the moment.
+
+2000-09-26  David Aspinall  <da@proofgeneral.org>
+
+	* ChangeLog.gz: Updated.
+
+	* etc/ProofGeneral.spec:
+	Fix adding af2 to RPM.
+
+	* Makefile.devel:
+	Remove extra space preventing ChangeLog update.
+
+	* etc/ProofGeneral.spec, html/devel.phtml, generic/proof-site.el, html/develdownload.phtml:
+	Set version tag for new release.
+
+	* html/main.phtml:
+	Link to Isar instead of Isar/README.
+
+	* images/goto.xpm: Make backgroundize
+
+	* html/main.phtml:
+	Fix Pauls web address
+
+	* html/oldnews.phtml, papers/README, html/about.phtml, html/cvsweb.conf, html/devel.phtml, generic/proof-utils.el, etc/ProofGeneral.spec, generic/proof-config.el, doc/README.doc, doc/ProofGeneral.texi, BUGS, FAQ, README, doc/PG-adapting.texi:
+	Fix Proof General web page to www.proofgeneral.org.
+
+	* etc/announce: Updated for 3.2 release
+
+	* html/develdownload.phtml: Typo
+
+2000-09-25  David Aspinall  <da@proofgeneral.org>
+
+	* etc/ProofGeneral.spec, html/devel.phtml, html/develdownload.phtml, generic/proof-site.el:
+	Set version tag for new release.
+
+	* Makefile.devel:
+	Remove twelf from .tar.gz
+
+	* etc/ProofGeneral.spec:
+	Add AF2 to RPM package.
+
+	* isa/todo:
+	Added bits from todo for Isabelle
+
+2000-09-25  Markus Wenzel  <wenzelm@informatik.tu-muenchen.de>
+
+	* isa/isabelle-system.el:
+	isa-isatool-command: tuned standard places of Isabelle installation;
+
+	* generic/proof-utils.el:
+	comment: avoid unbalanced quotes;
+
+2000-09-23  David Aspinall  <da@proofgeneral.org>
+
+	* etc/ProofGeneral.spec, html/devel.phtml, html/develdownload.phtml, generic/proof-site.el:
+	Set version tag for new release.
+
+	* TODO: Updated
+
+	* doc/ProofGeneral.texi: Update date.
+
+	* generic/proof-menu.el:
+	proof-display-some-buffers moves point to end of output in response buffer.
+
+	* html/news.phtml:
+	Forthcoming news item
+
+	* html/main.phtml:
+	Use prover-specific logos rather than generic ones...
+
+	* html/header.phtml:
+	Changed size of image
+
+	* html/develdownload.phtml: Minor
+
+	* todo: Removed:
+	  X Improve efficiency for processing for large proofs (N/A)
+	  D Enable toolbar in other PG buffers (done)
+	  A Add Pierre's improvement for X-Symbol config (done)
+	  A make C-c C-l go to bottom of response buffer while output (done)
+	  B New keymap(s) for proof assistants.  (done)
+	  A Add efficiency improvement by turning on/off prover output. (done)
+	  C Make the remaining options in the quick-opts-menu be more (done|N/A)
+
+	* html/images/isabelle.gif, html/images/coqlogo4.gif, html/images/coqlogo4.xcf:
+	Add prover-specific logo rather than generic ones...
+
+	* html/images/ProofGeneral.jpg, images/ProofGeneral.jpg:
+	Image of the general with ??? badge
+
+	* hol98/x-symbol-hol98.el, lego/x-symbol-lego.el:
+	Add Pierre's tweak
+
+	* twelf/x-symbol-twelf.el:
+	Standard poor X-Symbol support for twelf.
+
+	* todo:
+	Changes:  (actually in previous version)
+	- Undoing comments with FSF Emacs fixed (thanks to Christophe Raffalli)
+	- C-x C-v and C-x C-w supposed fixed.
+	- have added proof-shell-important-settings
+	- confused (initialization) bug: assumed fixed.
+	- proof-shell-handle-error-hook has gone
+	- rpm relocatability improved
+	- Added auto-autoloads
+	- proof-goals-display-qed-message has gone
+	- added mechanism to close goal....<nosave> goal.... sequences
+	- Removed unimportant X's:
+	  * X Consider filtering out special annotations from shell buffer
+
+	* images/goto.xbm: Deleted file
+
+	* generic/proof-menu.el:
+	proof-display-some-buffers improved: toggles between goals and response in
+	2-pane mode
+
+	* generic/proof-utils.el:
+	Fix proof-display-and-keep-buffer for displaying from non-script buffer.  Add proof-with-script-buffer.
+
+	* generic/span-overlay.el:
+	Always activate bug fix -- this file only loaded for FSF Emacs.
+
+	* generic/proof-toolbar.el:
+	Make toolbar enablers work appropriately from non-scripting buffers
+	Remove support for obsolete 1-bit xbm images
+	Update comments
+
+	* generic/proof-shell.el:
+	Call (proof-toolbar-setup) to add toolbar to goals and response buffer
+	Unify goals and response menus with script buffer menu
+
+	* images/use.xbm, images/undo.xbm, images/state.xbm, images/retract.xbm, images/restart.xbm, images/qed.xbm:
+	Deleted file
+
+	* generic/proof-script.el:
+	Remove require on proof-depends
+	Make toolbar commands work from non-scripting buffers
+	Add save file dialogue to proof-register-possibly-new-processed-file
+
+	* images/interrupt.xbm: Deleted file
+
+	* generic/proof-depends.el:
+	Update comments
+
+	* images/info.xbm: Deleted file
+
+	* generic/README: Updated
+
+	* images/help.xbm, images/goal.xbm:
+	Deleted file
+
+	* todo, INSTALL, CHANGES, BUGS:
+	Updated
+
+	* images/find.xbm, images/context.xbm, images/command.xbm, images/abort.xbm, images/next.xbm:
+	Deleted file
+
+	* images/goto.8bit.xpm, images/goto.xcf, images/goto.xpm:
+	Improved(?) goto button
+
+	* images/gimp/scripts/proofgeneral.scm:
+	Remove obsolete xbms
+
+	* images/Makefile: Remove xbm's
+
+2000-09-21  David Aspinall  <da@proofgeneral.org>
+
+	* doc/PG-adapting.texi:
+	Slightly shorter name for info dir entry.
+
+	* etc/ProofGeneral.spec, generic/proof-site.el, html/devel.phtml, html/develdownload.phtml:
+	Set version tag for new release.
+
+	* etc/ProofGeneral.spec:
+	Fix globbing some more.
+
+	* etc/ProofGeneral.spec:
+	Fix for rpm braindead globbing.
+
+	* doc/ProofGeneral.texi:
+	Fix infodir entry, it got broken somehow.
+
+	* etc/ProofGeneral.spec:
+	Add PG-adapting to info files.
+
+2000-09-21  Markus Wenzel  <wenzelm@informatik.tu-muenchen.de>
+
+	* isa/interface-setup.el:
+	tweak 'x-symbol-image-converter to avoid confusing warning;
+
+	* isar/interface, isa/interface:
+	use plain /bin/sh instead of bash;
+
+2000-09-21  David Aspinall  <da@proofgeneral.org>
+
+	* etc/ProofGeneral.spec:
+	Added Prefixes: tag
+
+	* Makefile.devel:
+	Add symlink PG -> PG-ver to main dist. Dont dereference symlinks when making tars (why was it done?).
+
+	* doc/Makefile:
+	Make PG-adapting first so index.html left pointing to main manual
+
+2000-09-21  Markus Wenzel  <wenzelm@informatik.tu-muenchen.de>
+
+	* isa/x-symbol-isabelle.el:
+	added Isabelle symbols for parendblleft/parendblright glyphs (will be
+	  present in X-Symbol-3.3e; should not cause problems with older
+	  versions);
+
+2000-09-21  David Aspinall  <da@proofgeneral.org>
+
+	* generic/proof-config.el: Newlines.
+
+	* images/abort.xcf, images/goal.8bit.xpm:
+	Tweaked abort button
+
+	* doc/PG-adapting.texi:
+	Improved adding more lisp code chapter.
+
+	* Makefile.devel:
+	Changed ChangeLog target to use rcs2log directly.  Added developer's details, correct emails.
+
+	* generic/proof-compat.el:
+	Removed blurry distinction between block-comment and comment in FSF's buffer-syntactic-context
+
+2000-09-21  Markus Wenzel  <wenzelm@informatik.tu-muenchen.de>
+
+	* isar/todo:
+	** D support proof-next-error?
+
+	* isar/isar.el: tuned comment;
+
+	* etc/isar/README:
+	bug2: Resolved as of 17.9.00;
+
+	* etc/screenshot-notes.txt:
+	fixed "Dagstuhl";
+
+	* todo: done: exit isar;
+	added comment about output performance;
+
+2000-09-20  Markus Wenzel  <wenzelm@informatik.tu-muenchen.de>
+
+	* isar/interface, isa/interface:
+	added -X option;
+
+2000-09-20  David Aspinall  <da@proofgeneral.org>
+
+	* ChangeLog.gz: Updated.
+
+	* etc/ProofGeneral.spec, html/devel.phtml, html/develdownload.phtml, generic/proof-site.el:
+	Set version tag for new release.
+
+	* generic/proof-script.el: Comments
+
+	* generic/proof-config.el:
+	Disable toolbar enablers on win32.
+
+	* images/abort.8bit.xpm, images/abort.xbm, images/abort.xpm:
+	New generated buttons.
+
+	* images/gimp/scripts/proofgeneral.scm:
+	Add new button
+
+2000-09-20  Christophe Raffalli  <Christophe.Raffalli@univ-savoie.fr>
+
+	* images/Makefile: added abort button
+
+	* images/abort.xcf: abort button
+
+	* generic/span-overlay.el:
+	dirty bug fix in next-span to avoid loops with FSF Emacs
+
+2000-09-19  Markus Wenzel  <wenzelm@informatik.tu-muenchen.de>
+
+	* isar/isar-syntax.el:
+	made \<> word characters (accomodates symbol representation);
+
+	* isar/interface, isa/interface:
+	installfonts only when using X window system;
+
+	* isar/isar.el:
+	isar-toolbar-entries: remove 'goal and 'qed;
+
+	* isar/isar-syntax.el: removed junk;
+
+	* isa/interface-setup.el:
+	improved xsymbol config: include info dir, only init for XEmacs;
+
+	* isa/todo:
+	done: ability to choose logic;
+
+	* isar/interface, isa/interface:
+	isa: DEFAULT_FILES="Scratch.thy Scratch.ML";
+
+	* isar/README: Isabelle version: 99-1;
+	tuned;
+
+	* isa/README: Isabelle version: 99-1;
+
+2000-09-18  Markus Wenzel  <wenzelm@informatik.tu-muenchen.de>
+
+	* isa/interface-setup.el:
+	more robust checking of xsymbol-home;
+
+2000-09-18  Christophe Raffalli  <Christophe.Raffalli@univ-savoie.fr>
+
+	* af2/af2-fun.el:
+	*** empty log message ***
+
+	* generic/proof-utils.el:
+	changed proof-remove-comment to avoid using string-search (using string-match instead).
+
+2000-09-18  David Aspinall  <da@proofgeneral.org>
+
+	* todo: Updated
+
+	* ChangeLog.gz: Updated.
+
+	* generic/proof-script.el:
+	Get rid of proof-segment-up-to-old.
+
+	* generic/proof-compat.el:
+	Added bug fix section and patch for undefined
+	font-lock-preprocessor-face in FSF Emacs.
+
+	* generic/proof-compat.el:
+	Emulate buffer-syntactic-context on FSF Emacs
+
+	* ChangeLog.gz: Updated.
+
+	* twelf/twelf-font.el:
+	Remove twelf-config-mode variable check, to allow functions
+	here to work with PG (without loading twelf-old.el).
+
+	* twelf/twelf.el:
+	Improvements to support: needs work in segment-up-to, though.
+
+2000-09-18  Markus Wenzel  <wenzelm@informatik.tu-muenchen.de>
+
+	* isar/isar-keywords.el:
+	complete set of keywords from IOA image;
+
+2000-09-18  David Aspinall  <da@proofgeneral.org>
+
+	* ChangeLog.gz: Updated.
+
+	* etc/ProofGeneral.spec, html/devel.phtml, html/develdownload.phtml, generic/proof-site.el:
+	Set version tag for new release.
+
+2000-09-17  Markus Wenzel  <wenzelm@informatik.tu-muenchen.de>
+
+	* isa/isa.el:
+	silent-cmd and init-cmd: activate Isabelle99-1 versions;
+
+	* isar/isar.el:
+	removed proof-shell-pre-sync-init-cmd (init now handled by -PI options
+	  in isabelle-command-line);
+	tuned comments;
+
+	* isa/isabelle-system.el:
+	isabelle-command-line: include -PI options for isar;
+	activate global-timing;
+
+	* isa/interface:
+	this file is now a COPY of isar/interface;
+
+	* isar/interface:
+	-I option for Isar vs. classic Isabelle mode;
+	tuned;
+
+2000-09-15  Markus Wenzel  <wenzelm@informatik.tu-muenchen.de>
+
+	* isa/interface, isar/interface:
+	isatool installfonts (for remote X-Symbol fonts);
+
+2000-09-15  Christophe Raffalli  <Christophe.Raffalli@univ-savoie.fr>
+
+	* af2/af2-font.el, af2/af2-fun.el, af2/af2.el:
+	various fixes.
+	.
+
+	* generic/proof-script.el:
+	added  proof-retract-current-goal
+
+	* generic/proof-script.el:
+	added proper call to proof-remove-comment before matching with proof-xxx-with-hole-regexp
+
+	* generic/proof-utils.el:
+	removed some debugging messages I forgot
+
+	* generic/proof-utils.el:
+	added function string-search and proof-remove-comment
+
+	* af2/af2.el:
+	major modifications including outline, atgs, ...
+
+	* af2/af2-outline.el:
+	outline minior mode definitions for af2
+
+	* af2/af2-font.el:
+	font-lock and sym-lock definitions for af2
+
+	* af2/af2-tags.el:
+	tags functions for af2
+
+	* af2/af2-fun.el:
+	usefull function definitions for af2
+
+2000-09-14  Markus Wenzel  <wenzelm@informatik.tu-muenchen.de>
+
+	* isa/x-symbol-isabelle.el:
+	renamed \<brokenbar> to \<bar>;
+	fixed glyph of \<pounds>;
+
+	* isa/x-symbol-isabelle.el:
+	x-symbol-isabelle-electric-ignore: "~=";
+
+2000-09-14  David Aspinall  <da@proofgeneral.org>
+
+	* ChangeLog.gz: Updated.
+
+	* etc/ProofGeneral.spec, html/devel.phtml, html/develdownload.phtml, generic/proof-site.el:
+	Set version tag for new release.
+
+	* doc/PG-adapting.texi:
+	Encourage use of easy instantiation mechanism.
+
+	* demoisa/demoisa-easy.el:
+	Encourage use of demoisa-easy.el
+
+	* generic/proof-script.el:
+	Remove FIXME.
+
+	* generic/proof-config.el:
+	Improved docstrings, comments.
+
+	* doc/ProofGeneral.texi:
+	Moved proof-add-completions to adapting manual
+
+	* doc/PG-adapting.texi:
+	Added doc of completions, several other script settings.  Sections in script chapter.
+
+	* doc/PG-adapting.texi:
+	Note about creating images for toolbar.
+
+	* etc/cvs-tips.txt, CHANGES, README.devel, todo:
+	Updated
+
+	* html/header.phtml, html/links.phtml, html/main.phtml, html/news.phtml, html/oldrel.phtml, html/register.phtml, html/download.phtml, html/elispmarkup.php3, html/features.phtml, html/about.phtml, html/devel.phtml:
+	Updates
+
+	* html/images/bullethole.gif:
+	Shrunk a bit
+
+	* images/notes.txt: Updated.
+
+2000-09-13  Markus Wenzel  <wenzelm@informatik.tu-muenchen.de>
+
+	* isar/todo:
+	done: make help key bindings appear in "Show me ..." menu;
+
+	* generic/proof-x-symbol.el:
+	capitalize xs-lang-name;
+
+2000-09-13  David Aspinall  <da@proofgeneral.org>
+
+	* ChangeLog.gz: Updated.
+
+	* doc/PG-adapting.texi:
+	Removed keystroke index.
+
+	* etc/ProofGeneral.spec, html/devel.phtml, html/develdownload.phtml, generic/proof-site.el:
+	Set version tag for new release.
+
+	* etc/isar/bad1.thy, etc/isar/bad2.thy, etc/isar/README:
+	Added some bug test cases.
+
+	* CHANGES, todo:
+	Updated
+
+	* Makefile:
+	Added af2 and twelf to elisp dirs.
+
+	* etc/release-log.txt:
+	Getting ready for 3.2 release
+
+	* html/functions.php3, html/gallery.phtml, html/header.phtml, html/develdownload.phtml, html/doc.phtml, html/download.phtml, html/features.phtml:
+	Minor changes and improvements
+
+	* html/images/pg-text.gif, html/images/ProofGeneral.jpg:
+	Reduced sizes of images.
+
+	* html/proofgen.css:
+	Revamp style a bit -- not so good with netscape but OK elsewhere.
+
+	* images/pg-text.gif, images/pg-text.xcf, images/ProofGeneral.gif, images/ProofGeneral.jpg, images/ProofGeneral.xcf:
+	Reduced sizes of images.
+
+	* doc/PG-adapting.texi:
+	Remove keystroke index, add appendix with demoisa code (directly included)
+
+	* generic/proof-config.el:
+	Docstring changes for printed docs.
+
+	* doc/PG-adapting.texi:
+	Add sections to chapter 2, and text on adjusting toolbar.  Update magic
+
+	* af2/af2.el:
+	Add removal of state button as test example. Replace af2-with-xemacs -> proof-running-on-XEmacs.
+
+	* af2/example.af2:
+	Add trivial test command.
+
+	* generic/proof-config.el: Order change
+
+	* generic/proof-toolbar.el:
+	Removed proof-toolbar-entries-default and <PA>-toolbar-entries.
+
+	* doc/PG-adapting.texi, doc/ProofGeneral.texi:
+	Minor improvements
+
+	* generic/proof-script.el:
+	Remove ambitious promise to implement proper generic-find-and-forget.
+
+	* generic/proof-config.el, generic/proof-toolbar.el:
+	Make <PA>-toolbar-entries, and move it and proof-toolbar-entries-default to proof-config to allow easier configuration.
+
+2000-09-12  David Aspinall  <da@proofgeneral.org>
+
+	* ChangeLog.gz: Updated.
+
+	* Makefile.devel:
+	Make ordinary dist before develdist, because dist clears build dir... whoops.
+
+	* ChangeLog.gz: Updated.
+
+	* etc/cvs-tips.txt:
+	Notes about using cvs remotely added.
+
+	* etc/ProofGeneral.spec, html/devel.phtml, html/develdownload.phtml, generic/proof-site.el:
+	Set version tag for new release.
+
+	* doc/PG-adapting.texi: Updated magic.
+
+	* doc/docstring-magic.el:
+	Add provide sym-lock to fix sym lock loading problem
+
+	* doc/PG-adapting.texi:
+	More details about parsing functions.  Improved intro
+
+	* doc/ProofGeneral.texi: Update date.
+
+	* generic/proof-script.el:
+	Remove shell important setting from script ones.
+
+	* af2/example.af2:
+	Rather empty example.
+
+	* af2/af2.el:
+	Add syntax config for block comments, and remove path from af2-prog-name.
+
+	* todo: Updated
+
+	* generic/proof-shell.el:
+	Add sanity check on important settings for proof shell (underway)
+
+	* generic/proof-site.el:
+	Added entry for Af2
+
+	* generic/proof-config.el:
+	Docs for proof-shell-eager-annotation-start stuff
+
+	* af2/af2.el:
+	New version sent by Christophe.
+
+2000-09-11  Markus Wenzel  <wenzelm@informatik.tu-muenchen.de>
+
+	* isa/isabelle-system.el:
+	proof-shell-pre-interrupt-hook for PolyML 3 only;
+
+2000-09-11  David Aspinall  <da@proofgeneral.org>
+
+	* ChangeLog.gz: Updated.
+
+	* etc/ProofGeneral.spec, html/devel.phtml, html/develdownload.phtml, generic/proof-site.el:
+	Set version tag for new release.
+
+	* af2/af2.el, af2/sym-lock.el:
+	New prover, first bash.
+
+	* generic/proof-config.el, generic/proof-script.el:
+	Added proof-shell-annotated-prompt-regexp to important settings, removed safe default of empty string (now will have error msgs from filter)
+
+2000-09-08  David Aspinall  <da@proofgeneral.org>
+
+	* doc/ProofGeneral.texi:
+	Customize always available if PG is
+
+	* todo: Updated
+
+	* isa/isabelle-system.el:
+	Changes for selecting object logic, locating executables.
+
+	* generic/proof-utils.el:
+	ADded proof-locate-executable.
+
+	* generic/proof-script.el:
+	Fix obscure problem with proof-segment-upto-cmdstart with buggy input.
+
+	* generic/proof-config.el:
+	Rearrangement
+
+2000-09-07  Markus Wenzel  <wenzelm@informatik.tu-muenchen.de>
+
+	* isar/isar-keywords.el:
+	removed "of", "congs";
+	added "hints";
+
+2000-09-03  Markus Wenzel  <wenzelm@informatik.tu-muenchen.de>
+
+	* isar/isar.el:
+	removed unused variable C;
+
+2000-09-02  Markus Wenzel  <wenzelm@informatik.tu-muenchen.de>
+
+	* isar/interface, isa/interface:
+	more quoting;
+
+2000-08-30  Markus Wenzel  <wenzelm@informatik.tu-muenchen.de>
+
+	* isar/isar.el: use isar-markup-ml;
+	eliminated superficial semicolons;
+	fixed proof-shell-quit-cmd;
+
+2000-08-29  Markus Wenzel  <wenzelm@informatik.tu-muenchen.de>
+
+	* isar/isar-syntax.el:
+	syntax: "?" made word char;
+
+2000-08-29  David Aspinall  <da@proofgeneral.org>
+
+	* ChangeLog.gz: Updated.
+
+	* etc/ProofGeneral.spec, generic/proof-site.el, html/devel.phtml, html/develdownload.phtml:
+	Set version tag for new release.
+
+	* html/news.phtml: Tweak
+
+	* twelf/example.elf:
+	Example file grabbed from twelf distrib
+
+	* twelf/twelf.el:
+	A little bit of progress.
+
+	* doc/PG-adapting.texi, generic/proof-config.el, generic/proof-shell.el:
+	Added proof-shell-auto-terminate-commands
+
+2000-08-28  David Aspinall  <da@proofgeneral.org>
+
+	* ChangeLog.gz: Updated.
+
+	* etc/ProofGeneral.spec, html/devel.phtml, html/develdownload.phtml, generic/proof-site.el:
+	Set version tag for new release.
+
+	* todo:
+	adapting manual needs intro fixing
+
+	* doc/ProofGeneral.texi:
+	Fix description of manual now broken into two
+
+	* doc/PG-adapting.texi: Updated magic
+
+	* doc/Makefile: Fix recursive make
+
+	* etc/cvs-tips.txt:
+	Note about CVSROOT setting.
+
+	* isa/isabelle-system.el: Branch
+
+	* isa/isabelle-system.el:
+	Remove Library.timings call, restore compatibility with I99.
+
+	* twelf/twelf.el, twelf/twelf-old.el, twelf/twelf-font.el:
+	Branch
+
+	* twelf/twelf.el, twelf/twelf-old.el, twelf/twelf-font.el:
+	Files for twelf, not working at all yet.
+
+	* TODO: Updated
+
+	* todo: Added a couple of todos
+
+	* isar/isar.el:
+	Change name of mode: isar-proofscript-mode -> isar-mode and remove
+	alias.  Regular mode name needed for fancy macros.
+
+	Use proof-definvisible fancy macro to define help menu functions.
+	Removed parentheses from menu entries so key bindings show up.
+
+	* doc/ProofGeneral.texi:
+	Missing full stop
+
+	* etc/isa/settings.ML:
+	Test file for proof-shell-set-elisp-variable-regexp
+
+	* isa/isa.el:
+	Added setting for proof-shell-set-elisp-variable-regexp
+
+	* generic/proof-shell.el, generic/proof-config.el:
+	Added proof-shell-set-elisp-variable-regexp
+
+	* generic/proof-site.el:
+	Added twelf and experimental support note.
+
+	* generic/proof-menu.el:
+	FIXME note added, missing docstring from macro fn def.
+
+	* html/news.phtml, html/oldnews.phtml:
+	News updated
+
+	* html/doc.phtml, html/develdownload.phtml:
+	Link to two manuals now.
+
+	* doc/README.doc, doc/localdir, doc/ProofGeneral.texi, doc/Makefile.doc, doc/PG-adapting.texi, doc/.cvsignore, doc/Makefile:
+	Split manual into two parts.
+
+	Added notes about find theorems trick of separating constants by comma
+	for Isabelle.  Made for version 99-1.
+
+	Improved documentation for urgent messages, including recent
+	additions.  Mentioned new high-level macros proof-defshortcut,
+	proof-definvisible.
+
+2000-08-28  Markus Wenzel  <wenzelm@informatik.tu-muenchen.de>
+
+	* isar/isar.el, isa/isa.el:
+	cd command: add_path;
+
+	* isa/interface-setup.el:
+	conditional load of proof-site.el;
+
+	* isar/interface, isa/interface:
+	-w false implies -x false;
+	do not load proof-site.el here;
+
+2000-08-26  Pierre Courtieu  <courtieu@lri.fr>
+
+	* coq/x-symbol-coq.el:
+	nothing important, I forgot to undo something before my last commit in
+	coq/x-symbol-coq.el
+
+	* coq/x-symbol-coq.el, coq/coq-syntax.el, coq/coq.el:
+	Some changes for undoing with coq, handle user-defined tactics, in
+	coq/coq-syntax.el and coq/coq.el.
+
+2000-08-23  Markus Wenzel  <wenzelm@informatik.tu-muenchen.de>
+
+	* isa/x-symbol-isabelle.el:
+	more symbols;
+
+	* isa/interface-setup.el:
+	tuned x-symbol setup;
+
+2000-08-16  Markus Wenzel  <wenzelm@informatik.tu-muenchen.de>
+
+	* isar/isar-syntax.el:
+	isar-keywords-proof-improper;
+
+	* isar/isar-keywords.el:
+	added isar-keywords-proof-improper;
+	tuned;
+
+2000-08-14  David Aspinall  <da@proofgeneral.org>
+
+	* generic/proof-depends.el:
+	Added Fiona's changes, cleaned up a little bit with header and footer
+
+	* generic/proof-shell.el:
+	Added split string on theorem dependency code, to make list of dependents.
+
+	* generic/proof-script.el:
+	Added Fiona's changes, cleaned up a little bit
+
+	* isa/thy-mode.el:
+	Added Fiona's changes.
+
+	* etc/isa/depends/Usedepends.ML, etc/isa/depends/Usedepends.thy, etc/isa/depends/Primes.ML, etc/isa/depends/Primes.thy, etc/isa/depends/Fib.ML, etc/isa/depends/Fib.thy:
+	Files for testing theorem dependency features.
+
+2000-08-14  Pierre Courtieu  <courtieu@lri.fr>
+
+	* coq/coq.el:
+	enhancement of outline regexps for coq, now when hiding bodies, we see
+	completely definitions and theorems, but proof script are hidden (but
+	can be blindly sent to the prover). Seems to work correctly.
+
+	* coq/x-symbol-coq.el:
+	enhancement of x-symbol for coq, philosophy is not encoded, and phi1 is,
+	one problem remains: a word ending with phi will be encoded.
+
+2000-08-09  Markus Wenzel  <wenzelm@informatik.tu-muenchen.de>
+
+	* isa/interface-setup.el:
+	smart setup of X-Symbol mode;
+
+2000-08-09  David Aspinall  <da@proofgeneral.org>
+
+	* ChangeLog.gz: Updated.
+
+	* etc/ProofGeneral.spec, html/devel.phtml, html/develdownload.phtml, generic/proof-site.el:
+	Set version tag for new release.
+
+2000-08-07  Markus Wenzel  <wenzelm@informatik.tu-muenchen.de>
+
+	* isar/isar-syntax.el:
+	added outline mode setup (still not quite working as expected);
+
+	* isar/isar.el:
+	cleaned up outline stuff;
+
+	* isar/isar-keywords.el:
+	new category isar-keywords-proof-heading;
+
+2000-08-03  Markus Wenzel  <wenzelm@informatik.tu-muenchen.de>
+
+	* isar/todo:
+	** B make help key bindings appear in "Show me ..." menu;
+
+	* isar/isar.el:
+	added isar-help functions / keys (how do I get keys into menus?);
+
+	* isa/x-symbol-isabelle.el:
+	x-symbol-isabelle-electric-ignore: include [[ ]];
+
+	* generic/proof-script.el:
+	handle comment inside a command (patch by da);
+
+2000-08-02  Markus Wenzel  <wenzelm@informatik.tu-muenchen.de>
+
+	* isa/x-symbol-isabelle.el:
+	x-symbol-isabelle-prepare-table: avoids redundancy in code, improves
+	  on isar version (only 1 backslash);
+
+	* isa/Example.ML, isa/Example.thy, isa/Example2.ML:
+	tuned;
+
+	* isa/isa.el: added isa-preprocessing;
+
+2000-07-29  Markus Wenzel  <wenzelm@informatik.tu-muenchen.de>
+
+	* isar/isar-syntax.el:
+	fixed isar-goals-font-lock-keywords;
+
+	* isar/isar-keywords.el:
+	added "thm_deps", "overloaded";
+
+2000-07-26  Markus Wenzel  <wenzelm@informatik.tu-muenchen.de>
+
+	* doc/ProofGeneral.texi: updated;
+
+	* doc/docstring-magic.el:
+	use proof-assistant-table instead of proof-assistants;
+
+2000-07-26  David Aspinall  <da@proofgeneral.org>
+
+	* ChangeLog.gz: Updated.
+
+	* etc/ProofGeneral.spec, html/devel.phtml, generic/proof-site.el, html/develdownload.phtml:
+	Set version tag for new release.
+
+	* isa/todo: Suggestion from DvO added
+
+2000-07-20  David Aspinall  <da@proofgeneral.org>
+
+	* etc/test-schedule.txt:
+	Note about need to test..
+
+2000-07-20  Markus Wenzel  <wenzelm@informatik.tu-muenchen.de>
+
+	* generic/proof-site.el:
+	proper evaluation of PROOFGENERAL_ASSISTANTS vs. proof-assistants;
+
+	* generic/proof-easy-config.el:
+	fixed comment;
+
+2000-07-20  David Aspinall  <da@proofgeneral.org>
+
+	* isa/isa.el:
+	Remove accidental testing setq left in.
+
+2000-07-19  David Aspinall  <da@proofgeneral.org>
+
+	* COPYING: Fix date
+
+	* generic/proof-shell.el:
+	bug fixing in matching theorem dependencies
+
+	* generic/proof-depends.el:
+	functions for manipulating theorem dependencies
+
+	* isa/isa.el, isa/depends.ML:
+	experiments with theorem dependencies
+
+	* generic/proof-shell.el, generic/proof-script.el, generic/proof-config.el:
+	changes to add theorem dependencies recording in spans
+
+2000-07-19  Markus Wenzel  <wenzelm@informatik.tu-muenchen.de>
+
+	* isar/isar.el:
+	use ML_command to avoid unwanted output;
+
+2000-07-19  David Aspinall  <da@proofgeneral.org>
+
+	* isa/isa.el: reverting to last version
+
+2000-07-19  fionam  <fionam@dcs.ed.ac.uk>
+
+	* isa/depends.ML, isa/isa.el:
+	file for theorem dependencies
+
+2000-07-17  Markus Wenzel  <wenzelm@informatik.tu-muenchen.de>
+
+	* CHANGES: tuned;
+
+2000-07-16  David Aspinall  <da@proofgeneral.org>
+
+	* ChangeLog.gz: Updated.
+
+	* etc/ProofGeneral.spec, html/devel.phtml, html/develdownload.phtml, generic/proof-site.el:
+	Set version tag for new release.
+
+	* coq/coq.el:
+	Removed some (hopefully redundant) requires.
+
+	* html/projects/pgml.html, html/projects/pgip.html:
+	Modified, now white paper contains DTDs (soon)
+
+	* papers/README:
+	Note that theres nothing there yet.
+
+2000-07-13  David Aspinall  <da@proofgeneral.org>
+
+	* ChangeLog.gz: Updated.
+
+	* etc/ProofGeneral.spec, generic/proof-site.el, html/devel.phtml, html/develdownload.phtml:
+	Set version tag for new release.
+
+	* etc/ProofGeneral.spec:
+	Add Isabelle interface scripts to RPM
+
+2000-07-12  David Aspinall  <da@proofgeneral.org>
+
+	* ChangeLog.gz: Updated.
+
+	* etc/ProofGeneral.spec, html/devel.phtml, html/develdownload.phtml, generic/proof-site.el:
+	Set version tag for new release.
+
+	* CHANGES, todo:
+	Updated
+
+	* doc/ProofGeneral.texi, html/about.phtml, html/feedback.phtml, html/gallery.phtml, html/proofgen.css, html/screenshot.phtml:
+	Minor updates
+
+	* generic/proof-autoloads.el:
+	Update autoloads.
+
+	* generic/proof-splash.el:
+	Make proof-splash-message autoload.
+
+2000-07-08  Markus Wenzel  <wenzelm@informatik.tu-muenchen.de>
+
+	* isa/isabelle-system.el:
+	isabelle-command-line: try to be smart in ensuring proper Isabelle
+	command line, avoiding nil under all circumstances;
+
+	* isar/isar.el:
+	proof-prog-name: use isabelle-command-line;
+	removed misc junk;
+
+	* isa/isa.el:
+	proof-prog-name: use isabelle-command-line;
+
+	* isa/interface-setup.el:
+	do not change isabelle-prog-name here;
+	be less aggressive in changing x-symbol-enable;
+
+2000-07-06  Markus Wenzel  <wenzelm@informatik.tu-muenchen.de>
+
+	* isar/isar.el:
+	tuned help-menu-entries;
+
+2000-07-05  David Aspinall  <da@proofgeneral.org>
+
+	* ChangeLog.gz: Updated.
+
+	* etc/ProofGeneral.spec, html/devel.phtml, html/develdownload.phtml, generic/proof-site.el:
+	Set version tag for new release.
+
+	* CHANGES: Updated
+
+	* isa/isa.el:
+	Fix to make back() undoable.
+
+2000-07-04  David Aspinall  <da@proofgeneral.org>
+
+	* ChangeLog.gz: Updated.
+
+	* etc/ProofGeneral.spec, html/devel.phtml, html/develdownload.phtml, generic/proof-site.el:
+	Set version tag for new release.
+
+	* html/cvsweb.conf, html/cvsweb.cgi:
+	CVS web script
+
+	* html/proofgen.css:
+	Changes for CVS web style fixup
+
+	* html/images/.cvsignore, html/images/silverrule.gif:
+	Ignore file for xvpics put there by gimp
+
+2000-07-03  David Aspinall  <da@proofgeneral.org>
+
+	* ChangeLog.gz: Updated.
+
+	* etc/ProofGeneral.spec, html/devel.phtml, generic/proof-site.el, html/develdownload.phtml:
+	Set version tag for new release.
+
+	* isa/isabelle-system.el:
+	Note about trapping errors
+
+	* todo: Updated
+
+2000-07-03  Markus Wenzel  <wenzelm@informatik.tu-muenchen.de>
+
+	* isa/isabelle-system.el:
+	quick-and-dirty t by default;
+
+2000-07-03  David Aspinall  <da@proofgeneral.org>
+
+	* isa/isabelle-system.el:
+	Patch to cope gracefully with empty list of Isabelle documents.
+
+2000-07-01  Markus Wenzel  <wenzelm@informatik.tu-muenchen.de>
+
+	* isa/isabelle-system.el:
+	activate global-timing;
+
+	* isar/isar.el: improved help menu;
+	replaced "help" by "welcome";
+
+	* isar/isar-keywords.el:
+	removed 'help';
+	added 'print_antiquotations', 'print_commands', 'print_trans_rules';
+
+	* isa/isabelle-system.el:
+	tuned docs menu;
+
+2000-06-30  Markus Wenzel  <wenzelm@informatik.tu-muenchen.de>
+
+	* isar/isar-keywords.el:
+	added method_setup;
+
+2000-06-29  David Aspinall  <da@proofgeneral.org>
+
+	* ChangeLog.gz: Updated.
+
+	* etc/ProofGeneral.spec, html/devel.phtml, html/develdownload.phtml, generic/proof-site.el:
+	Set version tag for new release.
+
+	* isa/isabelle-system.el:
+	Added quick-and-dirty setting -- we can still argue about the default, 8-)
+
+2000-06-27  David Aspinall  <da@proofgeneral.org>
+
+	* ChangeLog.gz: Updated.
+
+	* etc/ProofGeneral.spec, html/devel.phtml, generic/proof-site.el, html/develdownload.phtml:
+	Set version tag for new release.
+
+	* generic/span-overlay.el: Minor tweak.
+
+	* todo, TODO:
+	Updated
+
+	* isar/todo:
+	Note about typing in shell buffer
+
+	* isar/isar.el, isa/isa.el:
+	Tidy
+
+	* etc/isar/multiple/C.thy:
+	Added tag to force Isar mode
+
+2000-06-26  David Aspinall  <da@proofgeneral.org>
+
+	* generic/proof-script.el:
+	Fix mark buffer atomic problem (caused multiple file oddity with Isar), for new parsing functions.
+
+2000-06-22  David Aspinall  <da@proofgeneral.org>
+
+	* ChangeLog.gz: Updated.
+
+	* etc/ProofGeneral.spec, generic/proof-site.el, html/devel.phtml, html/develdownload.phtml:
+	Set version tag for new release.
+
+	* isa/Example.ML: Added missing proof.
+
+	* isar/Example.thy: Extra note.
+
+	* CHANGES: XEmacs only note
+
+	* FAQ:
+	Rearranged, more info about X-Sym probs
+
+	* generic/proof-shell.el:
+	Remove modeline from extra frames (in XEmacs).
+
+	* generic/proof-config.el:
+	Added back defconsts for face names needed for FSF Emacs.
+	Yet another annoyance with FSF.
+
+2000-06-22  Pierre Courtieu  <courtieu@lri.fr>
+
+	* coq/coq.el, coq/coq-syntax.el:
+	somme little changes to make undo work better
+
+2000-06-19  David Aspinall  <da@proofgeneral.org>
+
+	* ChangeLog.gz: Updated.
+
+	* etc/ProofGeneral.spec, html/devel.phtml, html/develdownload.phtml, generic/proof-site.el:
+	Set version tag for new release.
+
+	* isa/isabelle-system.el:
+	Fix typo causing missing proof-shell-pre-interrupt-hook.
+
+	* README.devel: Fix typo
+
+	* doc/ProofGeneral.texi:
+	Updated list of helpers.  Typo
+
+2000-06-16  Markus Wenzel  <wenzelm@informatik.tu-muenchen.de>
+
+	* isar/isar.el, isar/isar-syntax.el:
+	proper function-menu (fume) setup;
+
+	* isa/isa.el, isa/isa-syntax.el:
+	proper indentation setup;
+
+	* isa/Example.ML: proper indentation;
+
+	* generic/proof-script.el:
+	proof-script-find-next-entity: support list of match items;
+	replaced spurious re-search-forward by proof-re-search-forward;
+	proof-script-important-settings: commented out proof-goal-with-hole-regexp,
+	  proof-save-with-hole-regexp;
+
+	* generic/proof-config.el:
+	proof-script-next-entity-regexps: admit list of MATCHNOS;
+
+2000-06-16  David Aspinall  <da@proofgeneral.org>
+
+	* ChangeLog.gz: Updated.
+
+	* etc/ProofGeneral.spec, html/devel.phtml, generic/proof-site.el, html/develdownload.phtml:
+	Set version tag for new release.
+
+	* isa/x-symbol-isabelle.el:
+	Renamed x symbol language name to isabelle (rather big for status line, unfortunately)
+
+	* isa/isa.el, isa/isabelle-system.el, isar/isar.el:
+	Tuned x-symbol config, moved settings to isabelle-system.el
+
+	* generic/proof-config.el, generic/proof-x-symbol.el:
+	Added pgcustom x-symbol-language to allow different language name than proof assistant
+
+	* isar/x-symbol-isar.el: Deleted files.
+
+	* isa/x-symbol-isa.el, isa/x-symbol-isabelle.el:
+	Renamed file
+
+	* CHANGES:
+	Note about new indentation code and current buggy state
+
+2000-06-15  David Aspinall  <da@proofgeneral.org>
+
+	* todo:
+	Added new section on updates for future Emacs versions
+
+	* CHANGES: Updated
+
+	* isar/x-symbol-isar.el: Note to merge
+
+	* isa/isa.el:
+	First attempt at using new indentation for Isabelle.  Utterly broken.
+
+	* generic/proof-toolbar.el:
+	Support toolbar in gtk-xemacs
+
+	* generic/proof-x-symbol.el:
+	More comments at top of file
+
+	* README: Web addr note
+
+	* generic/proof-config.el:
+	Improved some docstrings.
+	Simplified face configuration by using auxiliary macro.
+	Now also works for gtk-xemacs.
+	Experimented with removing spurious face alias constants.
+
+	* doc/ProofGeneral.texi:
+	Elaborated on where to find example file
+
+2000-06-10  Markus Wenzel  <wenzelm@informatik.tu-muenchen.de>
+
+	* isar/todo: new indentation setup;
+
+2000-06-09  David Aspinall  <da@proofgeneral.org>
+
+	* ChangeLog.gz: Updated.
+
+	* INSTALL, todo:
+	Message about packages needed (incomplete)
+
+	* plastic/plastic.el:
+	Removed spurious requires.
+
+	* doc/ProofGeneral.texi: Updated magic.
+
+	* doc/docstring-magic.el:
+	Load a couple more file manually.
+
+	* generic/proof-shell.el:
+	Strange ? got in by accident.
+
+	* ChangeLog.gz: Updated.
+
+	* etc/ProofGeneral.spec, html/devel.phtml, generic/proof-site.el, html/develdownload.phtml:
+	Set version tag for new release.
+
+	* generic/proof-script.el: Comment
+
+	* CHANGES, generic/proof-shell.el:
+	Remove toolbar and menubar from windows in multiple frame mode.
+
+	* todo: Bug in file colouring
+
+2000-06-09  Markus Wenzel  <wenzelm@informatik.tu-muenchen.de>
+
+	* isa/isabelle-system.el:
+	fixed show_sorts;
+
+	* isar/isar.el:
+	proof-shell-error-regexp;
+
+2000-06-08  Markus Wenzel  <wenzelm@informatik.tu-muenchen.de>
+
+	* isar/isar.el: new indentation setup;
+	completion-table: use isar-keywords-major;
+
+	* isar/isar-syntax.el:
+	new indentation setup;
+
+	* isar/isar-keywords.el:
+	isar-keywords-proof-open/close;
+
+	* isar/Example.thy: proper indentation;
+
+	* plastic/plastic.el, isa/isa.el:
+	adapted to new indentation setup;
+
+	* generic/proof-indent.el:
+	rewrote code from scratch: faster, easier to configure; now enabled by default;
+
+	* generic/proof-config.el:
+	settings for new indentation setup;
+
+	* generic/proof-syntax.el:
+	added proof-looking-at-safe, proof-looking-at-syntactic-context;
+	removed proof-indent-commands-regexp;
+
+	* doc/ProofGeneral.texi:
+	completely new indentation setup: faster, easier to configure;
+	  now enabled by default;
+
+	* lego/lego.el:
+	basic setup for new indentation code;
+
+	* coq/example.v: proper indentation;
+
+	* coq/coq.el:
+	basic setup for new indentation code;
+
+	* todo:
+	Improved indentation code; enabled by default;
+
+2000-06-07  David Aspinall  <da@proofgeneral.org>
+
+	* isar/isar.el:
+	Failed attempted hack to support ML files in isar mode (see comments in isar-preprocessing).
+
+	* isa/isa.el:
+	Removed disable of simp tracing from enable/disable pr, desired functionality now in Isabelle's update_thy for PG
+
+2000-06-06  David Aspinall  <da@proofgeneral.org>
+
+	* ChangeLog.gz: Updated.
+
+	* etc/ProofGeneral.spec, generic/proof-site.el, html/devel.phtml, html/develdownload.phtml:
+	Set version tag for new release.
+
+	* todo: todo for C-c C-l to fix point
+
+	* Makefile.devel:
+	Make distclean rather than clean do the CVS pruning.
+
+	* generic/proof-script.el:
+	Added special hack for Isar to include proof-terminal-char in sent string.
+
+	* isar/isar.el:
+	Allowed ; to terminate a command by including it in regexp for cmdstart
+	Added completion for Isar keywords and X-symbol token names.
+
+2000-06-05  Markus Wenzel  <wenzelm@informatik.tu-muenchen.de>
+
+	* isar/isar-syntax.el:
+	isar-save-with-hole-regexp: proof-no-regexp;
+
+	* isar/isar.el:
+	proof-indent-commands-regexp: use proof-no-regexp;
+	isar-global-save-command-p: more robust wrt. empty prev span (malformed!?);
+	isar-preprocessing: fixed terminator regexp;
+
+	* isa/isabelle-system.el:
+	improved isabelle-verbatim-regexp: use \` \' instead of ^ $;
+
+	* generic/proof-syntax.el:
+	fixed proof-anchor-regexp: use \` instead of ^;
+	added proof-no-regexp;
+
+2000-06-05  David Aspinall  <da@proofgeneral.org>
+
+	* isar/isar-syntax.el:
+	Removed defunct comments
+
+	* isar/isar.el:
+	Temporary bug fix to solve nil span error message
+
+	* todo: Updated.
+
+	* CHANGES:
+	proof-next-error, proof-display-some-buffers
+
+	* doc/ProofGeneral.texi:
+	Added paragraph and index entry explaining prefix arguments,
+	and some more on keystrokes, for the Emacs-impoverished users.
+	Added doc of proof-display-some-buffers
+
+	* isa/thy-mode.el:
+	Added proof-next-error to menu.
+
+	* isa/isa.el:
+	Added settings for proof-next-error.
+	Added switch off of simplifier tracing to quiet command
+	(not good enough -- need help from Isabelle for that really).
+
+	* generic/proof-menu.el:
+	Added miscellaneous commands section, with proof-display-some-buffers
+	function.
+	Bind C-c C-l to proof-display-some-buffers, add to buffer menu.
+	Move start/exit to proof assistant specific menu.
+	Added proof-next-error to menu.
+
+	* generic/proof-utils.el:
+	proof-clean-buffer: clear next error flag if buffer is response.
+
+	* generic/proof-config.el:
+	Tweaked some docstrings.
+	Added proof-shell-next-error-regexp and friends.
+	Bind proof-shell-next-error in proof-universal-keys.
+
+	* generic/proof-shell.el:
+	Added proof-next-error.
+	proof-shell-invisible-command: add terminator if it seems to be
+	 missing (after all: it's useful for users with C-c C-v).
+
+	* generic/proof-autoloads.el:
+	Updated to add proof-next-error.
+
+2000-06-05  Markus Wenzel  <wenzelm@informatik.tu-muenchen.de>
+
+	* isa/isa-syntax.el:
+	fixed output syntax table;
+
+2000-06-04  Markus Wenzel  <wenzelm@informatik.tu-muenchen.de>
+
+	* generic/proof-script.el:
+	proof-segment-up-to-cmdstart/end: use proof-re-search, proof-looking-at!
+
+	* generic/proof-syntax.el:
+	proof-re-search-forward/backward: observe proof-case-fold-search;
+
+	* isa/isa-syntax.el:
+	replaced isa-verbatim by isabelle-verbatim;
+
+	* isa/isabelle-system.el:
+	added isabelle-verbatim;
+	fixed proof-shell-pre-interrupt-hook: use isabelle-verbatim;
+
+	* isar/isar.el:
+	replaced isar-verbatim by isabelle-verbatim;
+	added isar-strip-terminators;
+
+	* isar/todo: updated;
+
+	* isar/isar-syntax.el:
+	replaced isar-verbatim by isabelle-verbatim;
+	fixed output syntax table;
+
+	* generic/proof-script.el:
+	proof-segment-up-to-cmdstart: exclude leading blanks from command string;
+
+2000-06-03  Markus Wenzel  <wenzelm@informatik.tu-muenchen.de>
+
+	* generic/proof-script.el:
+	improved proof-segment-up-to-cmdstart: handle overlap of command
+	  prefix and comment/string (e.g. { vs {* in Isar);
+
+	* isar/isar-keywords.el: { } are back;
+
+2000-06-02  Pierre Courtieu  <courtieu@lri.fr>
+
+	* coq/coq.el:
+	Added 3 entries in the Coq menu: Print Check and Hints
+
+2000-06-01  David Aspinall  <da@proofgeneral.org>
+
+	* ChangeLog.gz: Updated.
+
+	* etc/ProofGeneral.spec, html/devel.phtml, generic/proof-site.el, html/develdownload.phtml:
+	Set version tag for new release.
+
+	* generic/proof-autoloads.el: Updated
+
+	* generic/proof-menu.el: Added autoload
+
+	* html/develdownload.phtml:
+	Added links to latest manual
+
+	* etc/isar/Parsing.thy:
+	File used to test new parsing mechanism.
+
+	* etc/pgkit/xmltest2.xml, etc/pgkit/xmltest1.xml:
+	New test files for PG kit.
+
+	* doc/ProofGeneral.texi:
+	Added proof-comment-{start,end}-regexp.
+	Added proof-segment-up-to-{cmdstart,cmdend} and details of
+	which is selected.
+	Updated magic.
+
+	* todo: Updated
+
+	* todo:
+	Note about generalizing settings mechanism
+
+	* coq/coq.el:
+	Removed time setting, added proof-assistant-settings-cmd to init string, but commented out
+
+	* coq/coq.el:
+	Added a couple of settings for Coq
+
+	* generic/proof-menu.el:
+	Allow two strings for boolean settings to handle non-uniformity in Coq
+
+	* generic/proof-config.el, generic/proof-shell.el:
+	Use proof-running-on-XEmacs variable.
+
+	* generic/proof-script.el:
+	Use proof-running-on-XEmacs variable.  Don't set proof-segment-up-to alias if already set.
+
+	* BUGS: Plea for debugging in FSF Emacs
+
+	* CHANGES:
+	Updated, mentioning new parsing function mechanisms
+
+	* isa/Example-Xsym.ML:
+	Remove spurious spaces
+
+	* isar/Example.thy:
+	Removed now spurious semicolons, 8-).
+
+	* isar/isar-keywords.el:
+	Temporarily removed keywords { and } for new parsing mechanism
+
+	* isar/isar.el:
+	Remove setting of proof-segment-up-to
+
+	* generic/pg-xml.el: New file
+
+	* generic/proof-script.el:
+	New parsing functions proof-segment-up-to-cmd{start,end}
+	Select new parsing function according to config variables
+	Use proof-comment-{start,end}-regexp, and set default values
+	in proof-config-done-related, from proof-comment-{start,end}
+	New proof-script-complete which uses proof-case-fold-search
+
+	* generic/proof-menu.el:
+	Changed 'complete to 'proof-script-complete to use proof-case-fold-search.
+
+	* generic/proof-shell.el:
+	Made require on proof-menu instead of proof-script.
+
+	* generic/proof-indent.el:
+	Use proof-comment-{start,end}-regexp
+
+	* generic/proof-config.el:
+	Added proof-comment-start-regexp, proof-commend-end-regexp.
+	Mention proof-script-complete in docstring for proof-case-fold-search.
+
+	* lego/lego.el:
+	Remove spurious requires.
+
+2000-05-31  David Aspinall  <da@proofgeneral.org>
+
+	* isa/isabelle-system.el:
+	Commented out global-timing since it seems to be Isabelle99-1 specific.
+
+	* isa/isa.el:
+	Added old completion table from Isamode.  Added code to automatically add completion for x-symbol tokens.
+
+	* generic/proof-menu.el:
+	Fix keybinding for completion.  Add completion to menubar.
+
+	* generic/proof-compat.el:
+	Added hack to completion.el to avoid adding every prefix as completion.
+
+	* generic/proof-x-symbol.el:
+	Compatibility with completion package.
+
+	* generic/proof-script.el:
+	Fixes for completion support.
+
+2000-05-30  Markus Wenzel  <wenzelm@informatik.tu-muenchen.de>
+
+	* isar/isar-syntax.el:
+	improved isar-goals-font-lock-keywords;
+
+2000-05-30  David Aspinall  <da@proofgeneral.org>
+
+	* ChangeLog.gz: Updated.
+
+	* etc/ProofGeneral.spec, generic/proof-site.el, html/devel.phtml, html/develdownload.phtml:
+	Set version tag for new release.
+
+	* isa/isa.el:
+	Added missing command terminators for proof-xsym commands
+
+	* generic/proof-script.el:
+	Hairy parsing for Isar.  Not finished (or working) yet.
+
+	* generic/proof-script.el:
+	Arg for proof-minibuffer-cmd: compact whitespace in region.
+
+	* generic/proof-script.el:
+	Fixed typo causing bug.  Generic parsing updated (still wip)
+
+2000-05-30  Markus Wenzel  <wenzelm@informatik.tu-muenchen.de>
+
+	* isa/interface-setup.el:
+	handle 'isa-x-symbol-enable vs. 'isar-x-symbol-enable;
+
+2000-05-30  David Aspinall  <da@proofgeneral.org>
+
+	* isar/isar.el:
+	isar-preprocessing inserts final terminator if none there.
+	Added (defpgdefault script-indent t) to turn on indentation.
+	Added proof-script-command-start-regexp setting.
+
+	* generic/proof-shell.el:
+	Change order of checks in proof-shell-live-buffer
+
+2000-05-30  Markus Wenzel  <wenzelm@informatik.tu-muenchen.de>
+
+	* isa/isabelle-system.el:
+	defpacustom global-timing;
+
+2000-05-30  David Aspinall  <da@proofgeneral.org>
+
+	* generic/proof-compat.el:
+	Added process-live-p
+
+	* generic/proof-config.el:
+	Added proof-script-command-start-regexp.  Updated docstrings to reflect that proof-terminal-char no longer appended to commands.
+
+	* generic/proof-indent.el: Tidied
+
+	* generic/proof-script.el:
+	Added doc of new prefix arg feature for proof-minibuffer-cmd
+
+	* generic/proof-script.el:
+	Added prefix arg to proof-minibuffer-cmd to insert current region.
+
+2000-05-29  David Aspinall  <da@proofgeneral.org>
+
+	* ChangeLog.gz: Updated.
+
+	* CHANGES:
+	Favourites mechanism now fully implemented, I hope.
+
+	* ChangeLog.gz: Updated.
+
+	* etc/ProofGeneral.spec, html/devel.phtml, html/develdownload.phtml, generic/proof-site.el:
+	Set version tag for new release.
+
+	* isa/isa-syntax.el: Docstring
+
+	* isar/isar-syntax.el:
+	Tweak font lock exprs enough for Example.thy
+
+	* isar/isar-syntax.el:
+	Font lock exprs for goals buffer like those in Isabelle
+
+	* isar/isar.el:
+	Set settings format function before calculating initial command.  Add hilit for goals buffer
+
+	* isa/isabelle-system.el:
+	Remove isar-markup-ml from here
+
+	* isar/isar.el:
+	Use generic default setting mechanism now.  Add isar-markup-ml here.
+
+	* isar/Example.thy:
+	Add -*- isar -*- tag to force mode, and comment to explain.
+
+	* CHANGES: Updated
+
+	* generic/proof-script.el:
+	Added new parsing mechanism.  Began removing proof-terminal-string.
+
+	* coq/coq.el, lego/lego.el:
+	Removed use of proof-terminal-string, added explicit terminators everywhere.
+
+	* todo: Updated
+
+	* etc/announce:
+	Updated for announcement.
+
+	* doc/ProofGeneral.texi:
+	Updated with new keybindings for Coq, Lego.
+
+	* lego/lego.el:
+	Changed keybindings for lego specific functions
+
+	* coq/coq.el:
+	Changed keybindings for coq specific functions
+
+	* isa/isabelle-system.el:
+	Generalized proof assistant settings mechanism
+
+	* isa/isa.el:
+	Add explicit terminators to commands.  Generalized isabelle-set-default-cmd.
+
+	* isa/isa-syntax.el:
+	Additions to font lock on output
+
+	* generic/proof-autoloads.el: Updated
+
+	* generic/proof-shell.el:
+	Don\'t wait for ever if process dies on startup
+
+	* generic/proof-syntax.el:
+	Generalized proof-format to allow sexps in replacement.
+
+	* generic/proof-indent.el:
+	Missing parenthesis
+
+	* generic/proof-utils.el:
+	Added functions for defining string and integer setters, for proof assistant settings.
+
+	* generic/proof-menu.el:
+	New stuff for making proof assistant settings.
+
+	* generic/proof-config.el:
+	Added configuration variables for proof assistant settings.  Docstring for favourites.
+
+	* generic/proof-compat.el:
+	Added replace-string for FSF.
+
+	* plastic/plastic.el:
+	Fixed define-key calls.  Set useful default for plastic prog name
+
+2000-05-26  David Aspinall  <da@proofgeneral.org>
+
+	* generic/proof-syntax.el: Docstring.
+
+	* lego/lego.el, isa/isabelle-system.el, coq/coq.el:
+	proof-defass-default -> defpgdefault
+
+	* generic/proof-script.el:
+	Removed proof-script-indent check.
+
+	* generic/proof-indent.el:
+	Update to use generic option indent-line, and switch inside
+	function rather than mode (so can be turned on/off easily).
+
+	* generic/proof-x-symbol.el:
+	Switch to using per-prover generic option for x-symbol-enable.
+
+	* generic/proof-menu.el:
+	Binding for complete.
+	Proper toggler use for generic option x symbol enable.
+
+	* generic/proof-utils.el:
+	Macros for generic custom settings from proof-config.
+	Made proof-set-value work with generic settings as well as global ones,
+	hacking a name for a generic function.
+
+	* generic/proof-config.el:
+	Rename proof-defass-custom -> defpgcustom.
+	Moved macros for generic custom settings to proof-utils.
+	Made proof-x-symbol-enable be generic (isa-x-symbol-enable, etc).
+	Ditto proof-script-indent.
+	Added proof-shell-pre-sync-init-cmd
+	Added PA-completion-table, PA-tags-program.
+
+2000-05-26  Paul Callaghan  <P.C.Callaghan@durham.ac.uk>
+
+	* plastic/plastic.el, plastic/test.lf:
+	fixed error in test.lf
+
+	fixed conflict in plastic.el
+
+2000-05-26  David Aspinall  <da@proofgeneral.org>
+
+	* generic/proof-compat.el:
+	Moved compatibility code into proof-compat.el
+
+	* generic/proof-site.el:
+	Only extend the load path if necessary
+
+	* Makefile.xemacs:
+	Comments, still nothing here.
+
+	* Makefile:
+	Clean also deletes CVS temporaries (naughty, should be in devel.clean really)
+
+	* todo: Updated
+
+	* doc/ProofGeneral.texi: Updated magic
+
+	* generic/texi-docstring-magic.el:
+	Attempt to quote @ (failed, dunno why)
+
+2000-05-26  Markus Wenzel  <wenzelm@informatik.tu-muenchen.de>
+
+	* isar/isar-syntax.el:
+	isar-any-command-regexp;
+
+	* isar/isar-keywords.el:
+	isar-keywords-major;
+
+2000-05-25  David Aspinall  <da@proofgeneral.org>
+
+	* ChangeLog.gz: Updated.
+
+	* generic/proof-config.el:
+	Temp hacks to get doc to build before proper commits.
+
+	* generic/proof-config.el:
+	Made x-symbol-enable be individual option.
+
+	* generic/proof-script.el:
+	Added completion table code.
+
+	* doc/docstring-magic.el:
+	Fixes for PA docs, and file load order.
+
+	* ChangeLog.gz: Updated.
+
+	* etc/ProofGeneral.patch:
+	Patched patch again.
+	Phew, what an effort.
+
+	* coq/coqtags:
+	Spurious newline causing patch to fall over.
+
+	* isar/isar.el:
+	Removed spurious code in isar-mode function.
+	Removed defunct key binding of C-c C-l (Overriden with goto-end-of-locked).
+
+	* ChangeLog.gz: Updated.
+
+	* etc/ProofGeneral.spec:
+	Fix applying of patch.
+
+	* ChangeLog.gz: Updated.
+
+	* etc/ProofGeneral.patch: Fix patch.
+
+	* etc/ProofGeneral.patch:
+	Updated patch.
+
+	* ChangeLog.gz: Updated.
+
+	* coq/coqtags, lego/legotags:
+	Revert to previous path for perl, better default for non-linux.  Linux uses RPM, where its fixed.
+
+	* ChangeLog.gz: Updated.
+
+	* doc/ProofGeneral.texi: Fix info bug.
+
+	* ChangeLog.gz: Updated.
+
+	* html/doc.phtml, Makefile.devel:
+	Make doc link to 3.1, not pre-release.  Minor extra editing on new release.
+
+	* doc/ProofGeneral.texi:
+	Doc more new features and bug fixes for 3.2.
+	Doc new PA-<name> mechanism.
+	Doc for completion.
+	Doc for proof-shell-pre-sync-init-cmd.
+
+	* CHANGES:
+	Note about proof-shell-pre-sync-init-cmd
+
+	* BUGS:
+	Note about fix for C-x C-f and friends
+
+	* etc/bug-notes.txt:
+	Note about sync problem
+
+	* lego/lego.el, isa/isa.el, isar/isar.el, generic/proof-shell.el, generic/proof-config.el:
+	Patch for synchronization problem in Coq, perhaps others.
+
+	* etc/README, etc/bug-notes.txt:
+	New file, test cases for bugs
+
+	* Makefile:
+	Add target for editing perl scripts too
+
+	* coq/coqtags, lego/legotags:
+	Change default path to perl
+
+	* ChangeLog.gz: Updated.
+
+	* html/news.phtml:
+	Second toolbar patch in 3.1.6 now.
+
+	* etc/release-log.txt:
+	Updated from 3.1 branch
+
+	* generic/proof-toolbar.el:
+	When button enablers disabled, don't use itimer or after-change hook.
+
+	* ChangeLog: Updated.
+
+	* etc/release-log.txt:
+	Second toolbar patch.
+
+	* generic/proof-toolbar.el:
+	When button enablers disabled, don't use itimer or after-change hook.
+
+	* ChangeLog.gz: Updated.
+
+	* CHANGES: Toolbar fixes.
+
+	* generic/proof-toolbar.el:
+	Next button is enabled whenever locked region is not full.
+
+	* ChangeLog.gz: Updated.
+
+	* html/develdownload.phtml: Minor
+
+	* etc/ProofGeneral.spec, generic/proof-site.el, html/devel.phtml, html/develdownload.phtml:
+	Set version tag for new release.
+
+	* html/links.phtml: Added link to HELM
+
+	* html/news.phtml: Fix para spacing
+
+	* html/news.phtml: Note about 3.1.6
+
+	* ChangeLog: Updated.
+
+	* generic/proof-site.el:
+	Set version tag for new release.
+
+	* generic/proof-config.el, etc/release-log.txt, doc/ProofGeneral.texi:
+	Turn off button enablers when running on Solaris
+
+2000-05-24  Markus Wenzel  <wenzelm@informatik.tu-muenchen.de>
+
+	* isar/isar-keywords.el: added "done";
+
+2000-05-22  Markus Wenzel  <wenzelm@informatik.tu-muenchen.de>
+
+	* isar/isar.el, isar/isar-syntax.el:
+	replaced proof-ids-to-regexp by isar-ids-to-regexp, which admits
+	keywords to consist of a single non-word char as well (e.g. { });
+
+	* isar/isar-keywords.el:
+	replaced {{ }} by { };
+
+2000-05-19  Markus Wenzel  <wenzelm@informatik.tu-muenchen.de>
+
+	* isar/isar-syntax.el, isar/isar.el:
+	isar-verbatim-regexp: include \n;
+
+2000-05-18  David Aspinall  <da@proofgeneral.org>
+
+	* todo:
+	Updated.  Noted that "first line" bug is more prevalent than thought.
+
+2000-05-18  Markus Wenzel  <wenzelm@informatik.tu-muenchen.de>
+
+	* isa/isa.el:
+	Goals.enable/disable_pr: improved version for Isabelle99-1 (commented out);
+
+2000-05-17  David Aspinall  <da@proofgeneral.org>
+
+	* ChangeLog.gz: Updated.
+
+	* generic/proof-menu.el:
+	Clarify favourites command: key sequence will begin with C-c C-a.
+
+	* ChangeLog.gz: Updated.
+
+	* etc/ProofGeneral.spec, html/devel.phtml, html/develdownload.phtml, generic/proof-site.el:
+	Set version tag for new release.
+
+	* html/papers/pgtalk.pdf: Updated
+
+2000-05-17  Markus Wenzel  <wenzelm@informatik.tu-muenchen.de>
+
+	* isa/isabelle-system.el:
+	added show-consts, long-names;
+	improved isar-markup-ml;
+
+	* isar/isar.el, isar/interface, isar/interface-setup.el:
+	re-use isa/interface-setup.el rather than separate isar version;
+
+2000-05-16  David Aspinall  <da@proofgeneral.org>
+
+	* ChangeLog.gz: Updated.
+
+2000-05-16  Pierre Courtieu  <courtieu@lri.fr>
+
+	* coq/coq.el:
+	debugging coq menu for old Xemacs compatibility, David said he will do this
+	for other provers (already done ?).
+
+2000-05-16  David Aspinall  <da@proofgeneral.org>
+
+	* lego/lego.el:
+	Fix buttons must be 3 long error (for 20.4 compatibility)
+
+	* ChangeLog.gz: Updated.
+
+	* html/doc.phtml: Reference tweak
+
+	* generic/proof-menu.el:
+	Fix buttons must be 3 long error
+
+	* ChangeLog.gz: Updated.
+
+	* etc/ProofGeneral.spec, html/devel.phtml, generic/proof-site.el, html/develdownload.phtml:
+	Set version tag for new release.
+
+	* generic/proof-utils.el: Docstring fix
+
+	* generic/proof-menu.el:
+	Fixes for defining favourites, added warning for pre-release users.
+
+	* doc/ProofGeneral.texi:
+	Updated magic, new funcs.
+
+	* doc/docstring-magic.el:
+	Fixed to load all files and define proof ass specifc vars.
+
+	* generic/proof-site.el:
+	Added proof-ready-for-assistant function to help docstring magic.
+
+	* FAQ: Added question asked by Larry.
+
+	* generic/proof-site.el: Comment added
+
+	* generic/proof-script.el:
+	Add proof-strict-state-preserving setting
+
+	* isa/interface-setup.el, isa/isabelle-system.el, isar/interface-setup.el:
+	Move setting of proof-shell-pre-interrupt-hook to isabelle-system.el
+
+	* isa/isabelle-system.el: Missing quote
+
+	* generic/proof-config.el:
+	Added version string to splash.  Added proof-strict-state-preserving
+
+	* todo:
+	Updated, mentioned Solaris bug reported by Markus.
+
+	* html/papers/pgtalk.pdf:
+	Updated PG talk slides
+
+	* html/doc.phtml:
+	Better reference to TACAS paper. Added link to white paper draft.
+
+	* Makefile:
+	Be more generous if bash is not found.
+
+	* Makefile:
+	Added scripts target to edit Isabelle scripts, patch from Mike Squire.
+
+2000-05-12  David Aspinall  <da@proofgeneral.org>
+
+	* doc/docstring-magic.el, todo:
+	Notes about fixing docstring-magic.
+
+	* todo: Updated
+
+	* isa/isabelle-system.el:
+	Fixup menus a bit.  Remove proof-prf on options change.
+
+	* isa/isa.el:
+	Remove proof-assistant-menu-entries, done generically now.
+
+	* isar/isar.el:
+	Modification of proof-shell-init-cmd.  Markus, please help...
+
+	* lego/lego.el:
+	Remove proof-assistant-menu-entries, done generically now.
+
+	* generic/proof-config.el:
+	Added proof-defassfun.  Comments
+
+	* generic/proof-menu.el:
+	Use (proof-ass X) instead of function call.
+
+	* isa/isabelle-system.el:
+	Several name changes isa- -> isabelle-, and made generic for Isar
+
+	* isa/isa.el: Comments
+
+	* CHANGES, generic/proof-menu.el:
+	Specific keys begin C-c C-a, not C-c a.
+
+	* generic/proof-menu.el, generic/proof-utils.el:
+	Moved utility functions to proof-utils.
+
+	* isa/isabelle-system.el:
+	Fix to menu definition.
+
+	* generic/proof-config.el:
+	Fix to function name
+
+	* lego/lego.el: Fix note.
+
+2000-05-11  David Aspinall  <da@proofgeneral.org>
+
+	* ChangeLog.gz: Updated.
+
+	* etc/ProofGeneral.spec, html/devel.phtml, html/develdownload.phtml, generic/proof-site.el:
+	Set version tag for new release.
+
+	* hol98/example.sml:
+	Explanatory comments
+
+	* lego/lego.el:
+	Changes and compatibility fixes for specific menu/keybindings.
+
+	* isar/isar.el:
+	Load isabelle-system file shared with Isabelle Proof General.
+	Add default settings to proof-shell-init-cmd.
+	Add Isabelle menu to menubar.
+
+	* isa/isabelle-system.el:
+	Generic help menu for Isabelle and Isabelle/Isar added.
+	Generalized option settings mechanism.
+	Added simplifier tracing flag.
+
+	* isa/isa.el:
+	Moved generic settings to isabelle-system.el. isa-set-default-cmd->isabelle-set..
+
+	* coq/coq.el:
+	Changes and compatibility fixes for specific menu/keybindings.
+
+	* CHANGES: Updated
+
+	* html/devel.phtml: Tidied page a bit
+
+	* generic/proof-shell.el:
+	Note abut ;;;###autoload not working for define-derived-mode.
+
+	* generic/proof-script.el:
+	Use proof-deftoggle macro.
+	Comments about failure for ;;;###autoload cookie for define-derived-mode
+	Attempted fixes for C-x C-w, C-x C-v, revert-buffer.
+
+	* generic/proof-utils.el:
+	Compatibility hack
+
+	* generic/proof-toolbar.el:
+	Use proof-deftoggle macro.
+
+	* generic/proof-site.el:
+	Fix for funnily named provers (Isabelle/Isar) and Emacs compatibility.
+
+	* generic/proof.el:
+	Extra arg to proof-splash-display-screen.
+
+	* generic/proof-menu.el:
+	Menus and code cleanup
+
+	* generic/proof-config.el:
+	Removed duplicate declaration
+
+	* generic/proof-splash.el:
+	Extra arg to proof-splash-display-screen to serve as an About box.
+
+	* generic/proof-config.el:
+	New mechanism for defining customization variables per-prover.
+
+	* FAQ: X-Symbol funny chars question
+
+	* etc/test-schedule.txt: Fixup branch
+
+	* etc/test-schedule.txt: New file
+
+2000-05-09  David Aspinall  <da@proofgeneral.org>
+
+	* ChangeLog.gz: Updated.
+
+	* README.devel: Updated
+
+	* html/news.phtml, html/devel.phtml:
+	Added browsable CVS.
+
+	* isa/todo:
+	Note about desirable additions to Isabelle
+
+	* isa/Example.ML: New goal.
+
+	* generic/proof-config.el:
+	New setting on the way...
+
+	* FAQ:
+	Added question about saving options
+
+	* ChangeLog.gz: Updated.
+
+	* etc/ProofGeneral.spec, html/devel.phtml, html/develdownload.phtml, generic/proof-site.el:
+	Set version tag for new release.
+
+	* CHANGES: Updated
+
+	* generic/proof-menu.el, generic/proof-config.el:
+	Fixup menus.
+
+	* generic/proof.el, generic/proof-site.el, generic/proof-autoloads.el, generic/proof-menu.el, generic/proof-script.el:
+	Fixup loading.
+
+	* isa/Example-Xsym.ML: New file
+
+	* html/projects/xmlpgip.html:
+	New project (unlinked yet)
+
+	* generic/proof-script.el:
+	Removed menus, keybinding.  Removed compatibility hacks.  Improved loading.
+
+	* generic/proof-shell.el:
+	Improved loading
+
+	* generic/proof-config.el:
+	Prevent proof-set-value until proof-config-loaded. (C) on splash screen.
+
+	* generic/texi-docstring-magic.el:
+	Improved loading
+
+	* generic/span-extent.el, generic/span-overlay.el:
+	Comments.
+
+	* generic/proof.el:
+	Removed autoloads, util functions.
+
+	* generic/proof-x-symbol.el:
+	Improved loading
+
+	* generic/proof-utils.el:
+	Added some functions for developers.
+
+	* generic/proof-toolbar.el:
+	Improved loading
+
+	* generic/proof-system.el: Fixup branch
+
+	* generic/proof-system.el:
+	Moved code to proof-menu.el
+
+	* generic/proof-syntax.el:
+	Added proof-splice-separator.
+
+	* generic/proof-splash.el:
+	Splash screen now shown from autoloaded function.
+
+	* generic/proof-site.el:
+	Remove use of cl.  Add require on proof-autoloads.
+
+	* generic/proof-easy-config.el, generic/proof-indent.el:
+	Improve loading
+
+	* generic/span.el, generic/proof-autoloads.el, generic/proof-compat.el, generic/proof-menu.el:
+	Fixup branch
+
+	* generic/span.el, generic/proof-autoloads.el, generic/proof-menu.el, generic/proof-compat.el:
+	New files
+
+	* etc/cvs-tips.txt: Trivial.
+
+	* doc/ProofGeneral.texi:
+	Updated 3.2 changes
+
+	* Makefile.devel:
+	Added autoloads target.
+
+	* Makefile: EMACS -> BATCHEMACS var
+
+	* ChangeLog: Updated.
+
+	* etc/release-log.txt, isa/isa.el:
+	Merged from 3.1.5
+
+	* etc/release-log.txt: Updated
+
+	* generic/proof-site.el:
+	Set version tag for new release.
+
+	* isa/isa.el:
+	Generalized thms_containing
+
+	* doc/Makefile: Added default target
+
+2000-05-07  David Aspinall  <da@proofgeneral.org>
+
+	* generic/proof-config.el: Comments
+
+2000-05-05  David Aspinall  <da@proofgeneral.org>
+
+	* isa/isa.el: Comment.
+
+	* doc/ProofGeneral.texi:
+	Updated 3.2 details.  Keybindings for Coq, LEGO shortcuts changed.
+
+	* ChangeLog.gz: Updated.
+
+	* html/news.phtml: Missing para
+
+	* html/news.phtml: Buglet in html
+
+	* ChangeLog.gz: Updated.
+
+	* etc/ProofGeneral.spec, html/devel.phtml, generic/proof-site.el, html/develdownload.phtml:
+	Set version tag for new release.
+
+	* doc/ProofGeneral.texi:
+	Fix markup bug.
+
+	* doc/ProofGeneral.texi:
+	Expanded explanation of selecting Isar.
+
+	* todo: Updated
+
+	* Makefile:
+	make clean removes Emacs backups.  Probably safe...
+
+	* html/news.phtml: Hot news about FAQ.
+
+	* CHANGES: Updated
+
+	* isa/isa.el, isa/isabelle-system.el:
+	isa-system.el -> isabelle-system.el
+
+	* isa/isa-system.el, isa/isabelle-system.el:
+	Renamed file
+
+	* isa/thy-mode.el: Expanded menu
+
+	* generic/proof-script.el:
+	Comments.  Minor improvements for electric terminator and proof-follow-mode='ignore
+
+	* generic/proof-shell.el:
+	Corrected header.
+
+	* generic/proof.el:
+	Moved code into proof-system and proof-utils.
+
+	* generic/proof-system.el:
+	Files for interfacing with proof system, e.g. maintaining settings.
+
+	* generic/proof-utils.el:
+	General utility functions, moved from proof.el
+
+	* generic/proof-toolbar.el:
+	Added menu entry for proof-goto-end-of-locked.
+
+	* generic/proof-site.el:
+	Added variables for customization groups so they can be set automatically.
+
+	* generic/proof-config.el:
+	Improved docs, declaration of variables set in proof-site, settings mechanism begun.
+
+	* isa/isa.el:
+	New code in isa-system.el.
+
+	* isa/isa-system.el:
+	New file for interfacing with Isabelle system.
+
+	* isa/isa.el, isar/isar.el:
+	Default to isa-mode or isar-mode according to first one invoked.
+
+	* FAQ: Beginnings of a FAQ.
+
+2000-05-02  David Aspinall  <da@proofgeneral.org>
+
+	* plastic/plastic.el, isa/Example.ML, lego/example.l, lego/lego.el, generic/proof-syntax.el, generic/proof.el, generic/proof-config.el, generic/proof-script.el, CHANGES, coq/coq.el:
+	Added proof-assistant-keymap and commands for defining insert keys.
+
+2000-05-01  David Aspinall  <da@proofgeneral.org>
+
+	* CHANGES: Cease mentioning plastic.
+
+	* ChangeLog.gz: Updated.
+
+	* generic/proof.el: Helper macros.
+
+	* lego/lego.el:
+	Added specific menu for LEGO.
+
+	* ChangeLog.gz: Updated.
+
+	* etc/ProofGeneral.spec, html/devel.phtml, generic/proof-site.el, html/develdownload.phtml:
+	Set version tag for new release.
+
+	* isa/isa.el:
+	Added specific menu for Isabelle (early version)
+
+	* coq/coq.el:
+	Added specific menu for Coq.
+
+	* CHANGES, doc/ProofGeneral.texi, generic/proof-config.el, generic/proof-script.el:
+	Added proof-assistant-menu-entries for proof assistant specific menus.
+
+	* html/develdownload.phtml: Trivial
+
+	* BUGS, todo:
+	Added note about new FSF bug discovered, sigh...
+
+2000-04-28  David Aspinall  <da@proofgeneral.org>
+
+	* Makefile.devel: Force in .gz target.
+
+	* ChangeLog.gz: Updated.
+
+	* Makefile.devel:
+	Keep ChangeLog gzipped.  Small saving on repo size.
+
+	* ChangeLog, ChangeLog.gz:
+	Renamed/gzipped file.
+
+	* ChangeLog: Updated.
+
+	* etc/ProofGeneral.spec, html/devel.phtml, generic/proof-site.el, html/develdownload.phtml:
+	Set version tag for new release.
+
+	* etc/cvs-tips.txt:
+	Note about conflict in merging
+
+	* html/news.phtml, etc/release-log.txt:
+	Added note about 3.1.4 patch, merged from 3.1 branch
+
+	* etc/README, etc/cvs-tips.txt:
+	Notes about using cvs and branch.
+
+	* Makefile.devel:
+	Added warning about releasing from old branch.
+
+	* ChangeLog: Updated.
+
+	* html/news.phtml, etc/release-log.txt:
+	Note about 3.1.4 release
+
+	* ChangeLog: Updated.
+
+	* generic/proof-site.el:
+	Set version tag for new release.
+
+	* isa/isa.el, generic/proof-syntax.el:
+	Apply patch sent by Mike Squire
+
+2000-04-26  David Aspinall  <da@proofgeneral.org>
+
+	* ChangeLog: Updated.
+
+	* etc/ProofGeneral.spec, html/devel.phtml, html/develdownload.phtml, generic/proof-site.el:
+	Set version tag for new release.
+
+2000-04-25  Markus Wenzel  <wenzelm@informatik.tu-muenchen.de>
+
+	* isar/isar.el:
+	isar-indent regexps moved to isar-syntax.el;
+	tuned comments;
+
+	* isar/isar-syntax.el:
+	removed unused isar-ids;
+	added isar-indent regexps (from isar.el);
+
+	* isar/isar-keywords.el:
+	removed "simpset" minor keyword;
+
+2000-04-25  David Aspinall  <da@proofgeneral.org>
+
+	* html/main.phtml:
+	20.X -> recent, since XEmacs now on 21.
+
+	* generic/proof-syntax.el:
+	Fix %r modifier in proof-format-filename.
+
+	* isa/isa.el:
+	Revert to indended fix for isa-retract-thy-file.
+
+	* CHANGES, generic/proof-script.el:
+	Note about efficiency/bug fix by Markus.
+
+2000-04-17  Markus Wenzel  <wenzelm@informatik.tu-muenchen.de>
+
+	* isa/isa.el:
+	fixed isa-retract-thy-file: pass theory name only;
+	fixed some comments;
+
+	* isar/isar-keywords.el: added 'hide';
+
+2000-04-15  Markus Wenzel  <wenzelm@informatik.tu-muenchen.de>
+
+	* generic/proof-script.el:
+	proof-segment-up-to: no longer poke around in make-string buffer (now
+	  more efficient, also works around crash bug in xemacs-21.1.7/SuSE);
+
+2000-04-12  Markus Wenzel  <wenzelm@informatik.tu-muenchen.de>
+
+	* isar/isar.el:
+	fixed proof-mode-for-goals;
+
+2000-04-07  David Aspinall  <da@proofgeneral.org>
+
+	* lego/readonly/readonly.l:
+	Fix version.
+
+	* ChangeLog: Updated.
+
+	* Makefile.devel:
+	Change order in release to make ChangeLog be updated before dist built.
+
+	* ChangeLog: Updated.
+
+	* doc/ProofGeneral.texi:
+	mode-for-pbp -> mode-for-goals
+
+	* etc/ProofGeneral.spec, html/devel.phtml, html/develdownload.phtml, generic/proof-site.el:
+	Set version tag for new release.
+
+	* generic/proof-shell.el: Comment.
+
+	* todo: Updated
+
+	* generic/proof-script.el:
+	More generic message to avoid confusion with Coq searching.
+
+	* generic/proof-config.el:
+	Generalisation of proof-info-command to string or fn.
+
+	* lego/readonly/readonly.l:
+	Moved from wrong place.
+
+	* generic/pbp.el: Removed this.
+
+	* todo, CHANGES:
+	Updated
+
+	* generic/proof-x-symbol.el, generic/proof-shell.el, generic/proof-easy-config.el:
+	pbp-mode -> goals-mode
+
+	* generic/proof-config.el:
+	Comments. pbp-mode -> goals-mode
+
+	* isa/isa.el:
+	Tweak to disable_pr function to allow for it being called twice (why?).
+
+	* plastic/plastic.el:
+	pbp-mode -> goals-mode
+
+	* hol98/hol98.el: Decoration tweaks
+
+	* demoisa/demoisa.el, isar/isar.el, isa/isa.el, coq/coq.el:
+	pbp-mode -> goals-mode
+
+	* coq/coq-syntax.el: More decoration
+
+	* lego/lego.el: goals-mode -> pbp-mode
+
+	* lego/lego-syntax.el:
+	Extra decoration.
+
+	* doc/ProofGeneral.texi:
+	Updates for 3.2.  Added documentation of silent settings.
+
+	* plastic/plastic.el, generic/proof-shell.el, generic/proof-config.el, demoisa/demoisa-easy.el, demoisa/demoisa.el, lego/lego.el, coq/coq.el, hol98/hol98.el, isa/BUGS, isa/isa.el, todo, CHANGES:
+	Fixed up proof-shell-proof-completed mess nicely.
+
+2000-04-06  Markus Wenzel  <wenzelm@informatik.tu-muenchen.de>
+
+	* isar/x-symbol-isar.el, isa/x-symbol-isa.el:
+	tuned \<bottom>;
+	added \<lbrace>, \<rbrace>, \<top>;
+
+2000-04-05  Markus Wenzel  <wenzelm@informatik.tu-muenchen.de>
+
+	* isar/todo, isa/todo:
+	tuned todo stuff;
+
+	* isar/isar.el, isa/isa.el:
+	improved print_mode switch;
+
+	* isar/isar-keywords.el:
+	'welcome' made diagnostic;
+
+	* isar/isar-keywords.el:
+	eliminated 'as' keyword;
+
+2000-04-04  Markus Wenzel  <wenzelm@informatik.tu-muenchen.de>
+
+	* isar/isar-keywords.el:
+	added 'print_claset', 'print_simpset';
+
+2000-04-04  David Aspinall  <da@proofgeneral.org>
+
+	* ChangeLog: Updated.
+
+	* isa/isa.el:
+	Added provisional commands for enabling/disabling printing.
+
+	* ChangeLog: Updated.
+
+	* etc/ProofGeneral.spec, html/devel.phtml, generic/proof-site.el, html/develdownload.phtml:
+	Set version tag for new release.
+
+	* todo: Updated
+
+	* isa/Example2.ML:
+	Save as Example.ML, except using X-Symbol input tokens.
+
+	* CHANGES: Note of 3.2 changes
+
+	* generic/proof-script.el:
+	Improved behaviour of electric terminator.
+
+	* todo: Updated
+
+	* generic/proof-shell.el:
+	Added implementation of silent switch for turning on/off prover output.
+
+	* generic/proof-shell.el:
+	Added proof-shell-clear-state function to collect together state clearing ops.
+
+	* html/devel.phtml, CHANGES:
+	Updates for 3.2 series.
+
+	* html/projects/reelcase.html, html/projects.phtml:
+	Added new project B4
+
+	* ChangeLog: Updated.
+
+	* generic/proof-site.el:
+	Set version tag for new release.
+
+	* html/oldnews.phtml, html/news.phtml:
+	Updated news about 3.1.3, split old news out.
+
+	* etc/release-log.txt:
+	Note about 3.1.3 release
+
+	* isa/isa.el:
+	Fix accidently introduced bug with passing full paths to theory loader.
+
+	* generic/proof-syntax.el:
+	Altered proof-format-filename to add %e and %r specifiers.
+
+	* generic/proof.el, generic/proof-splash.el, generic/proof-script.el, generic/proof-easy-config.el, generic/proof-config.el, generic/proof-shell.el:
+	Update copyright dates, comments.
+