path: root/ChangeLog

2002-07-18  David Aspinall  <da@proofgeneral.org>

	* etc/coq/queryreplace.v:
	Record bug as solved.

	* etc/coq/queryreplace.v: New files.

	* doc/ProofGeneral.texi:
	Mention how to enable X-Symbol.

	* FAQ: Add FAQ about enabling X-Symbol.

	* etc/isar/XSymbolTests.thy: More tests

	* etc/isar/XSymbolTests.thy:
	More comments on current bugs

	* etc/isar/XSymbolTests.thy: New files.

	* doc/ProofGeneral.texi:
	More on keybindings: include old x-symbol-isabelle bindings but using super.

	* ChangeLog: Updated.

	* BUGS: Update

	* ChangeLog: Updated.

	* Makefile.devel:
	Try to fix latest link

	* etc/ProofGeneral.spec:
	fix README rename.

	* ChangeLog: Updated.

	* etc/ProofGeneral.spec:
	Set version tag for new release.

	* etc/ProofGeneral.spec:
	Rename READMEs for different provers so dont clash with doc directive.

	* CHANGES: Mention experimental nature

	* doc/PG-adapting.texi: Update magic

	* doc/ProofGeneral.texi:
	Update magic, move version history to appendix.

	* etc/release-log.txt, etc/announce:
	Update towards 3.4

	* CHANGES, BUGS:
	Mention known probs in prerel

2002-07-18  David Aspinall  <da@proofgeneral.org>

	* BUGS: Update

	* ChangeLog: Updated.

	* Makefile.devel:
	Try to fix latest link

	* etc/ProofGeneral.spec:
	fix README rename.

	* ChangeLog: Updated.

	* etc/ProofGeneral.spec:
	Set version tag for new release.

	* etc/ProofGeneral.spec:
	Rename READMEs for different provers so dont clash with doc directive.

	* CHANGES: Mention experimental nature

	* doc/PG-adapting.texi: Update magic

	* doc/ProofGeneral.texi:
	Update magic, move version history to appendix.

	* etc/release-log.txt, etc/announce:
	Update towards 3.4

	* CHANGES, BUGS:
	Mention known probs in prerel

2002-07-18  David Aspinall  <da@proofgeneral.org>

	* Makefile.devel:
	Try to fix latest link

	* etc/ProofGeneral.spec:
	fix README rename.

	* ChangeLog: Updated.

	* etc/ProofGeneral.spec:
	Set version tag for new release.

	* etc/ProofGeneral.spec:
	Rename READMEs for different provers so dont clash with doc directive.

	* CHANGES: Mention experimental nature

	* doc/PG-adapting.texi: Update magic

	* doc/ProofGeneral.texi:
	Update magic, move version history to appendix.

	* etc/release-log.txt, etc/announce:
	Update towards 3.4

	* CHANGES, BUGS:
	Mention known probs in prerel

2002-07-18  David Aspinall  <da@proofgeneral.org>

	* etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el:
	Set version tag for new release.

	* etc/ProofGeneral.spec:
	Rename READMEs for different provers so dont clash with doc directive.

	* html/doc.html: Fix typo

	* html/doc.html:
	Use short cut links for manual, and remove 3.3 from doc links.

	* html/functions.php3:
	hack_html: Make internal links use short-cut url if given

	* html/adaptingman, html/userman:
	New files.

	* html/devel.html, html/main.html:
	Link to standalone comps

	* html/develdownload.php:
	Link to latest version for manuals

	* html/components.html:
	Add links for TeXinfo and docstrings

	* html/components, html/components.html:
	New files.

	* CHANGES: Mention experimental nature

	* isa/isabelle-system.el, isar/isar.el, generic/proof-utils.el, isa/isa.el, generic/pg-goals.el, generic/proof-config.el:
	Fix active variable highlighting in Isabelle with X-Symbol.

	* doc/PG-adapting.texi: Update magic

	* doc/ProofGeneral.texi:
	Update magic, move version history to appendix.

	* html/doc.html:
	Add links to Emacs manuals.

	* html/links.html: Fix link to ETI

	* etc/release-log.txt, etc/announce:
	Update towards 3.4

	* CHANGES, BUGS:
	Mention known probs in prerel

2002-07-17  David Aspinall  <da@proofgeneral.org>

	* generic/proof-script.el:
	Add note about proof-generic-state-preserving-p

	* html/features.html:
	Improve feature list.

	* ChangeLog: Updated.

	* etc/ProofGeneral.spec, generic/proof-site.el, html/develdownload.php, html/devel.html:
	Set version tag for new release.

	* html/news.html, html/develdownload.php, todo:
	Updates

	* CHANGES: Mention term highlighting

	* isa/isa.el:
	Support subterm help facility (not quite working)

	* isar/isar.el:
	Support subterm help facility

	* isa/todo, phox/README, coq/README, coq/todo, isar/todo:
	Update versions/TODO

	* generic/pg-goals.el:
	Added subterm help popup facility

	* generic/span-extent.el:
	Add span-string.

	* generic/proof-shell.el:
	Add proof-shell-invisible-cmd-get-result

	* generic/proof-config.el:
	Add pg-subterm-help-cmd

	* generic/proof-script.el: Cleanups

	* generic/span-overlay.el:
	Fix span-string, span-object

2002-07-16  David Aspinall  <da@proofgeneral.org>

	* lego/lego.el, lego/lego-syntax.el, phox/phox.el, plastic/plastic.el, isa/isa.el, isar/isar.el, generic/proof-syntax.el, generic/proof-utils.el, generic/proof-compat.el, generic/proof-config.el, generic/proof-shell.el, etc/lego/pbp.l, generic/pg-goals.el, generic/pg-response.el, generic/pg-user.el, doc/ProofGeneral.texi, demoisa/demoisa.el, doc/PG-adapting.texi, coq/coq.el:
	Refactor several variable names; clean up, doc subterm markup and output display.

	* isa/isabelle-system.el: Fix typo.

	* isa/isabelle-system.el:
	Add conversion of idmarkup to subterm

2002-07-17  David Aspinall  <da@proofgeneral.org>

	* etc/ProofGeneral.spec, generic/proof-site.el, html/develdownload.php, html/devel.html:
	Set version tag for new release.

	* html/news.html, html/develdownload.php, todo:
	Updates

	* CHANGES: Mention term highlighting

	* isa/isa.el:
	Support subterm help facility (not quite working)

	* isar/isar.el:
	Support subterm help facility

	* isa/todo, phox/README, coq/README, coq/todo, isar/todo:
	Update versions/TODO

	* generic/pg-goals.el:
	Added subterm help popup facility

	* generic/span-extent.el:
	Add span-string.

	* generic/proof-shell.el:
	Add proof-shell-invisible-cmd-get-result

	* generic/proof-config.el:
	Add pg-subterm-help-cmd

	* generic/proof-script.el: Cleanups

	* generic/span-overlay.el:
	Fix span-string, span-object

2002-07-16  David Aspinall  <da@proofgeneral.org>

	* lego/lego.el, lego/lego-syntax.el, phox/phox.el, plastic/plastic.el, isa/isa.el, isar/isar.el, generic/proof-syntax.el, generic/proof-utils.el, generic/proof-compat.el, generic/proof-config.el, generic/proof-shell.el, etc/lego/pbp.l, generic/pg-goals.el, generic/pg-response.el, generic/pg-user.el, doc/ProofGeneral.texi, demoisa/demoisa.el, doc/PG-adapting.texi, coq/coq.el:
	Refactor several variable names; clean up, doc subterm markup and output display.

	* isa/isabelle-system.el: Fix typo.

	* isa/isabelle-system.el:
	Add conversion of idmarkup to subterm

	* ChangeLog: Updated.

	* etc/isar/Parsing.thy:
	Add { and } example

	* Makefile.devel: Fix crucial typo

	* ChangeLog: Updated.

	* Makefile.devel:
	Make tags for both manuals.

	* Makefile.devel:
	Tweak link creation/deletion

	* CHANGES: Minor

	* todo: Updated

	* etc/Mailman/note.txt: Updated.

	* html/register: Buggy tag

	* html/proofgen.css:
	Fix monospace typeface name

	* isar/isar.el: Add more nags

	* html/main.html: Edit for brevity

	* html/head.html:
	Use linked style sheet, add charset metatag.

	* generic/span-overlay.el:
	Dodgy patch to fix selection ordering of overlays. PBP works in Emacs now.

	* isa/x-symbol-isabelle.el:
	Patch so works without x-symbol

	* etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el:
	Set version tag for new release.

	* Makefile.devel: Link in LATESTNAME

	* generic/proof.el: Fix comment

	* generic/pg-goals.el, generic/pg-response.el, generic/proof-shell.el:
	Refactoring

	* generic/proof-x-symbol.el: Comments

	* isar/isar.el:
	Revert some premature changes in x-sym support

	* isa/x-symbol-isabelle.el:
	Merge patches from Christoph, and add Isabelle/Isar capabilities

	* generic/proof-compat.el:
	Add char-to-int and friends, borrowed from x-symbol-emacs.

	* generic/proof-shell.el:
	Cleaning up PBP code

	* etc/lego/pbp.l: Example of using pbp

2002-07-16  David Aspinall  <da@proofgeneral.org>

	* etc/isar/Parsing.thy:
	Add { and } example

	* Makefile.devel: Fix crucial typo

	* ChangeLog: Updated.

	* Makefile.devel:
	Make tags for both manuals.

	* Makefile.devel:
	Tweak link creation/deletion

	* CHANGES: Minor

	* todo: Updated

	* etc/Mailman/note.txt: Updated.

	* html/register: Buggy tag

	* html/proofgen.css:
	Fix monospace typeface name

	* isar/isar.el: Add more nags

	* html/main.html: Edit for brevity

	* html/head.html:
	Use linked style sheet, add charset metatag.

	* generic/span-overlay.el:
	Dodgy patch to fix selection ordering of overlays. PBP works in Emacs now.

	* isa/x-symbol-isabelle.el:
	Patch so works without x-symbol

	* etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el:
	Set version tag for new release.

	* Makefile.devel: Link in LATESTNAME

	* generic/proof.el: Fix comment

	* generic/pg-goals.el, generic/pg-response.el, generic/proof-shell.el:
	Refactoring

	* generic/proof-x-symbol.el: Comments

	* isar/isar.el:
	Revert some premature changes in x-sym support

	* isa/x-symbol-isabelle.el:
	Merge patches from Christoph, and add Isabelle/Isar capabilities

	* generic/proof-compat.el:
	Add char-to-int and friends, borrowed from x-symbol-emacs.

	* generic/proof-shell.el:
	Cleaning up PBP code

	* etc/lego/pbp.l: Example of using pbp

2002-07-16  David Aspinall  <da@proofgeneral.org>

	* Makefile.devel:
	Make tags for both manuals.

	* Makefile.devel:
	Tweak link creation/deletion

	* CHANGES: Minor

	* todo: Updated

	* etc/Mailman/note.txt: Updated.

	* html/register: Buggy tag

	* html/proofgen.css:
	Fix monospace typeface name

	* isar/isar.el: Add more nags

	* html/main.html: Edit for brevity

	* html/head.html:
	Use linked style sheet, add charset metatag.

	* generic/span-overlay.el:
	Dodgy patch to fix selection ordering of overlays. PBP works in Emacs now.

	* isa/x-symbol-isabelle.el:
	Patch so works without x-symbol

	* etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el:
	Set version tag for new release.

	* Makefile.devel: Link in LATESTNAME

	* generic/proof.el: Fix comment

	* generic/pg-goals.el, generic/pg-response.el, generic/proof-shell.el:
	Refactoring

	* generic/proof-x-symbol.el: Comments

	* isar/isar.el:
	Revert some premature changes in x-sym support

	* isa/x-symbol-isabelle.el:
	Merge patches from Christoph, and add Isabelle/Isar capabilities

	* generic/proof-compat.el:
	Add char-to-int and friends, borrowed from x-symbol-emacs.

	* generic/proof-shell.el:
	Cleaning up PBP code

	* etc/lego/pbp.l: Example of using pbp

2002-07-15  David Aspinall  <da@proofgeneral.org>

	* etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el:
	Set version tag for new release.

	* Makefile.devel:
	Do not link devel release.  Fix releasefinal to do that.

	* html/download.html:
	Cleanup, details on versions

	* html/screenshot, html/screenshot.html, html/index.php, html/news.html:
	Fix

	* html/features.html: Tweak

	* html/functions.php3:
	Add stuff for alternative DTD

	* html/main.html: Put isa first

	* html/header.html: Fix link, tag.

2002-07-14  David Aspinall  <da@proofgeneral.org>

	* etc/Mailman/note.txt: Updated.

	* etc/Mailman/intro-proofgeneraldevel.html, etc/Mailman/intro-proofgeneral.html:
	Add links

	* html/mailinglist:
	Mention developers list too

	* etc/Mailman/listinfo.html:
	Remove spurious white space

	* html/proofgen.css:
	font-series -> weight fixes.

	* etc/Mailman/intro-proofgeneral.html, etc/Mailman/intro-proofgeneraldevel.html:
	New files.

	* ChangeLog: Updated.

	* Makefile.devel: Flag on cp

	* ChangeLog: Updated.

	* hol98/hol98.el: ws

	* twelf/twelf.el: Remove use new parser

	* todo: Stick 3.4 stuff on end

	* isa/BUGS, isar/BUGS, BUGS:
	Tracing bug

	* html/oldrel.php: Add check changes

	* doc/ProofGeneral.texi: Fix authorship

	* Makefile.devel: Add prune to update

	* Makefile.devel: Try to debug

	* ChangeLog: Updated.

	* etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el:
	Set version tag for new release.

	* html/develdownload.php: Reformat

	* html/mailinglist: Typo

	* html/download.html:
	Remove 3.3 download, encourage test version use.

	* html/news.html: Rewrite history

	* html/oldrel.php: Move 3.3 to oldrel

	* html/devel.html: Improve layout

	* html/proofgen.css: Tweaks for forms.

	* html/feedback.php: Improve layout.

	* html/main.html:
	Simplify system infos.

	* html/images/phox-einstein.jpg:
	New files.

	* demoisa/demoisa-easy.el:
	Layout, comments.

	* html/features.html, html/main.html:
	Move project desc to features listing

	* html/register: Improve layout

	* html/proofgen.css:
	Style for lists tweaked.

	* etc/Mailman/note.txt: New files.

	* etc/Mailman/subscribe.html, etc/Mailman/handle_opts.html, etc/Mailman/listinfo.html, etc/Mailman/options.html:
	Cleanup html, fix URLs to final versions.

2002-07-13  David Aspinall  <da@proofgeneral.org>

	* etc/Mailman/subscribe.html, etc/Mailman/handle_opts.html:
	First customized versions

	* etc/Mailman/options.html:
	Fix up.  Still ugly.

	* etc/Mailman/handle_opts.html, etc/Mailman/subscribe.html, etc/Mailman/options.html:
	New files.

	* etc/Mailman/listinfo.html:
	Tidy up source, improve titles.

2002-07-14  David Aspinall  <da@proofgeneral.org>

	* Makefile.devel: Flag on cp

	* ChangeLog: Updated.

	* hol98/hol98.el: ws

	* twelf/twelf.el: Remove use new parser

	* todo: Stick 3.4 stuff on end

	* isa/BUGS, isar/BUGS, BUGS:
	Tracing bug

	* html/oldrel.php: Add check changes

	* doc/ProofGeneral.texi: Fix authorship

	* Makefile.devel: Add prune to update

	* Makefile.devel: Try to debug

	* ChangeLog: Updated.

	* etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el:
	Set version tag for new release.

	* html/develdownload.php: Reformat

	* html/mailinglist: Typo

	* html/download.html:
	Remove 3.3 download, encourage test version use.

	* html/news.html: Rewrite history

	* html/oldrel.php: Move 3.3 to oldrel

	* html/devel.html: Improve layout

	* html/proofgen.css: Tweaks for forms.

	* html/feedback.php: Improve layout.

	* html/main.html:
	Simplify system infos.

	* html/images/phox-einstein.jpg:
	New files.

	* demoisa/demoisa-easy.el:
	Layout, comments.

	* html/features.html, html/main.html:
	Move project desc to features listing

	* html/register: Improve layout

	* html/proofgen.css:
	Style for lists tweaked.

	* etc/Mailman/note.txt: New files.

	* etc/Mailman/subscribe.html, etc/Mailman/handle_opts.html, etc/Mailman/listinfo.html, etc/Mailman/options.html:
	Cleanup html, fix URLs to final versions.

2002-07-13  David Aspinall  <da@proofgeneral.org>

	* etc/Mailman/subscribe.html, etc/Mailman/handle_opts.html:
	First customized versions

	* etc/Mailman/options.html:
	Fix up.  Still ugly.

	* etc/Mailman/handle_opts.html, etc/Mailman/subscribe.html, etc/Mailman/options.html:
	New files.

	* etc/Mailman/listinfo.html:
	Tidy up source, improve titles.

2002-07-14  David Aspinall  <da@proofgeneral.org>

	* hol98/hol98.el: ws

	* twelf/twelf.el: Remove use new parser

	* todo: Stick 3.4 stuff on end

	* isa/BUGS, isar/BUGS, BUGS:
	Tracing bug

	* html/oldrel.php: Add check changes

	* doc/ProofGeneral.texi: Fix authorship

	* Makefile.devel: Add prune to update

	* Makefile.devel: Try to debug

	* ChangeLog: Updated.

	* etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el:
	Set version tag for new release.

	* html/develdownload.php: Reformat

	* html/mailinglist: Typo

	* html/download.html:
	Remove 3.3 download, encourage test version use.

	* html/news.html: Rewrite history

	* html/oldrel.php: Move 3.3 to oldrel

	* html/devel.html: Improve layout

	* html/proofgen.css: Tweaks for forms.

	* html/feedback.php: Improve layout.

	* html/main.html:
	Simplify system infos.

	* html/images/phox-einstein.jpg:
	New files.

	* demoisa/demoisa-easy.el:
	Layout, comments.

	* html/features.html, html/main.html:
	Move project desc to features listing

	* html/register: Improve layout

	* html/proofgen.css:
	Style for lists tweaked.

	* etc/Mailman/note.txt: New files.

	* etc/Mailman/subscribe.html, etc/Mailman/handle_opts.html, etc/Mailman/listinfo.html, etc/Mailman/options.html:
	Cleanup html, fix URLs to final versions.

2002-07-13  David Aspinall  <da@proofgeneral.org>

	* etc/Mailman/subscribe.html, etc/Mailman/handle_opts.html:
	First customized versions

	* etc/Mailman/options.html:
	Fix up.  Still ugly.

	* etc/Mailman/handle_opts.html, etc/Mailman/subscribe.html, etc/Mailman/options.html:
	New files.

	* etc/Mailman/listinfo.html:
	Tidy up source, improve titles.

2002-07-14  David Aspinall  <da@proofgeneral.org>

	* etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el:
	Set version tag for new release.

	* html/develdownload.php: Reformat

	* html/mailinglist: Typo

	* html/download.html:
	Remove 3.3 download, encourage test version use.

	* html/news.html: Rewrite history

	* html/oldrel.php: Move 3.3 to oldrel

	* html/devel.html: Improve layout

	* html/proofgen.css: Tweaks for forms.

	* html/feedback.php: Improve layout.

	* html/main.html:
	Simplify system infos.

	* html/images/phox-einstein.jpg:
	New files.

	* demoisa/demoisa-easy.el:
	Layout, comments.

	* html/features.html, html/main.html:
	Move project desc to features listing

	* html/register: Improve layout

	* html/proofgen.css:
	Style for lists tweaked.

	* etc/Mailman/note.txt: New files.

	* etc/Mailman/subscribe.html, etc/Mailman/handle_opts.html, etc/Mailman/listinfo.html, etc/Mailman/options.html:
	Cleanup html, fix URLs to final versions.

2002-07-13  David Aspinall  <da@proofgeneral.org>

	* etc/Mailman/subscribe.html, etc/Mailman/handle_opts.html:
	First customized versions

	* etc/Mailman/options.html:
	Fix up.  Still ugly.

	* etc/Mailman/handle_opts.html, etc/Mailman/subscribe.html, etc/Mailman/options.html:
	New files.

	* etc/Mailman/listinfo.html:
	Tidy up source, improve titles.

	* etc/Mailman/listinfo.html: New files.

	* html/functions.php3:
	Fix link in mozilla in click_to_go_back.

	* html/header.html:
	Change colour but not boldness

	* html/download.html:
	Remove length rant

	* html/proofgen.css: Fix typo

	* html/register: Improve form

	* html/about.html: Triv

	* html/projects/mm.html:
	Link to page mentioned by emacs guy

	* html/mailinglist:
	Remove extra hr, use h3

	* html/functions.php3:
	Use proofgeneral.org mailing addresses again.

	* html/smallheader.html:
	Reduce size to keep it smaller than main header

	* html/mailinglist:
	Fix mailman links, remove subscription form from here.

	* html/devel.html: Fix link

	* html/screenshot.html:
	Fix layout a bit

	* html/devel.html:
	Tweak mailing list details, order of items.

	* html/header.html:
	Compress header, shrink images

	* html/about.html:
	Reorder, include links here.

	* html/images/pg-text.gif: Reformat

	* html/head.html: Add favicon to head

	* images/notes.txt:
	Add note about favicon.

	* html/favicon.ico: New files.

	* html/images/favicon.ico: Deleted file

	* html/images/favicon.ico: New files.

2002-07-12  David Aspinall  <da@proofgeneral.org>

	* generic/proof-shell.el: Trivial

	* generic/proof-script.el:
	condition-case -> ignore-errors, comment.

	* BUGS:
	Mention probs with tracing mode.

	* etc/isar/Parsing.thy:
	Add some nesting examples

2002-07-02  David Aspinall  <da@proofgeneral.org>

	* html/doc.html:
	Give link to develdownload for latest docs

	* doc/ProofGeneral.texi:
	Remove description of known bugs.

	* isar/isar-syntax.el:
	Remove FIXME: have added definition of font-lock-preprocessor-face

	* generic/proof-compat.el:
	Add definition of font-lock-preprocessor-face

2002-07-01  David Aspinall  <da@proofgeneral.org>

	* ChangeLog: Updated.

	* html/news.html: Syntax error

	* doc/ProofGeneral.texi, doc/PG-adapting.texi:
	Updates for 3.4

	* ChangeLog: Updated.

	* etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el:
	Set version tag for new release.

	* html/news.html: Fix date on news item

	* generic/proof-utils.el:
	Use executable-find

	* generic/proof-script.el:
	proof-restart: also remove idiom internal spans.

	* generic/proof-x-symbol.el:
	Fix problem with GNU Emacs support: switch to multibyte in output buffers

	* isa/x-symbol-isabelle.el:
	Doc difference between isa and isar, fix prob with isa support.

	* isa/isabelle-system.el:
	Added isabelle-load-isar-keywords mimic of script startup.

	* isar/isar-syntax.el:
	Adjust syntax tables.

	* isar/isar.el:
	Adjust load order, and try to load a good isar-keywords file.  Add several FIXMEs.

	* isar/test.el:
	Add code to test new parser.

2002-06-30  David Aspinall  <da@proofgeneral.org>

	* isar/isar-keywords.el:
	Revert to previous version.  Explain existence of other versions

2002-07-01  David Aspinall  <da@proofgeneral.org>

	* html/news.html: Syntax error

	* doc/ProofGeneral.texi, doc/PG-adapting.texi:
	Updates for 3.4

	* ChangeLog: Updated.

	* etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el:
	Set version tag for new release.

	* html/news.html: Fix date on news item

	* generic/proof-utils.el:
	Use executable-find

	* generic/proof-script.el:
	proof-restart: also remove idiom internal spans.

	* generic/proof-x-symbol.el:
	Fix problem with GNU Emacs support: switch to multibyte in output buffers

	* isa/x-symbol-isabelle.el:
	Doc difference between isa and isar, fix prob with isa support.

	* isa/isabelle-system.el:
	Added isabelle-load-isar-keywords mimic of script startup.

	* isar/isar-syntax.el:
	Adjust syntax tables.

	* isar/isar.el:
	Adjust load order, and try to load a good isar-keywords file.  Add several FIXMEs.

	* isar/test.el:
	Add code to test new parser.

2002-06-30  David Aspinall  <da@proofgeneral.org>

	* isar/isar-keywords.el:
	Revert to previous version.  Explain existence of other versions

2002-07-01  David Aspinall  <da@proofgeneral.org>

	* etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el:
	Set version tag for new release.

	* html/news.html: Fix date on news item

	* generic/proof-utils.el:
	Use executable-find

	* generic/proof-script.el:
	proof-restart: also remove idiom internal spans.

	* generic/proof-x-symbol.el:
	Fix problem with GNU Emacs support: switch to multibyte in output buffers

	* isa/x-symbol-isabelle.el:
	Doc difference between isa and isar, fix prob with isa support.

	* isa/isabelle-system.el:
	Added isabelle-load-isar-keywords mimic of script startup.

	* isar/isar-syntax.el:
	Adjust syntax tables.

	* isar/isar.el:
	Adjust load order, and try to load a good isar-keywords file.  Add several FIXMEs.

	* isar/test.el:
	Add code to test new parser.

2002-06-30  David Aspinall  <da@proofgeneral.org>

	* isar/isar-keywords.el:
	Revert to previous version.  Explain existence of other versions

	* README: Update version

	* CHANGES: Update, cleanup

	* BUGS:
	Reorg.  Mention fontification bug.

	* pgkit/README: New files.

	* generic/proof-script.el:
	Fix error catching in proof-deactivate-scripting-auto.

	* generic/proof-splash.el:
	Robustify form GNU Emacs

	* isa/x-symbol-isabelle.el:
	Fix x-symbol-isabelle-input-token-grammar to remove spurious backslashes

	* isa/isa-syntax.el:
	Fix GNU Emacs/X-Symbol compatibility for sml-sym-face added by Lucas Dixon.

	* etc/isar/Persistent.thy: New files.

	* generic/proof-script.el, generic/proof-shell.el:
	When killing process or scripting buffer, register file if it is complete, rather than always retracting.

	* generic/proof-shell.el:
	proof-shell-kill-function: deactivate scripting before shutting down prover

2002-06-24  David Aspinall  <da@proofgeneral.org>

	* generic/proof-x-symbol.el:
	Require x-symbol-vars as recommended for new version (works with old too?)

	* generic/proof-menu.el:
	Disable fly past comments for old parser again.

	* generic/proof-config.el:
	Default to using old parser for now.

	* generic/proof-config.el, generic/proof-script.el:
	use-old-parser setting replaces use-new-parser setting [WARNING: big change]

	* generic/proof-compat.el:
	Also use our own buffer-syntactic-context in XEmacs 21.4.

	* isa/Example.ML, isa/Example.thy:
	Add Emacs mode comments at top

	* isa/thy-mode.el:
	Move auto-mode-alist hack here now Isar is default.

	* isa/isa.el: Fix comment

	* isa/x-symbol-isabelle.el:
	[TESTING] support for latest version of X-Symbol (back compat broken).

	* isa/isabelle-system.el:
	Hack to avoid loading x-symbol-isabelle

	* isar/isar-keywords.el:
	Fix to prevent {* being considered a command, flag edits

	* isar/isar.el:
	Remove auto-mode-alist hack, and require on x-symbol-isabelle [TESTING].

2002-06-21  David Aspinall  <da@proofgeneral.org>

	* FAQ:
	Wrong: mustn't delete isa dir, files shared with isar.

	* twelf/twelf.el, lego/lego.el, lego/lego-syntax.el, lego/x-symbol-lego.el, isar/isar.el, isar/isar-syntax.el, isa/x-symbol-isabelle.el, isa/isa.el, isa/isa-syntax.el, isa/thy-mode.el, acl2/acl2.el, html/download.html:
	GPL update

	* doc/PG-adapting.texi, doc/ProofGeneral.texi:
	GPL, 3.4 dates

	* CHANGES, COPYING:
	GPL

	* FAQ: Isar is default over isa.

	* generic/span.el, generic/span-extent.el, generic/span-overlay.el, generic/texi-docstring-magic.el, generic/proof.el, generic/proof-system.el, generic/proof-toolbar.el, generic/proof-utils.el, generic/proof-x-symbol.el, generic/proof-site.el, generic/proof-splash.el, generic/proof-syntax.el, generic/proof-shell.el, generic/proof-depends.el, generic/proof-easy-config.el, generic/proof-indent.el, generic/proof-menu.el, generic/proof-script.el, generic/pg-xhtml.el, generic/pg-xml.el, generic/proof-compat.el, generic/proof-config.el, generic/pg-metadata.el, generic/pg-pgip.el, generic/pg-user.el:
	GPL

	* BUGS: Mention looping GNU

2002-06-20  David Aspinall  <da@proofgeneral.org>

	* ChangeLog: Updated.

	* etc/ProofGeneral.spec, generic/proof-site.el, html/develdownload.php, html/devel.html:
	Set version tag for new release.

2002-06-20  David Aspinall  <da@proofgeneral.org>

	* etc/ProofGeneral.spec, generic/proof-site.el, html/develdownload.php, html/devel.html:
	Set version tag for new release.

2002-06-19  Pierre Courtieu  <courtieu@lri.fr>

	* CHANGES, doc/ProofGeneral.texi:
	Updated the doc and the CHANGES file about new backtracking for Coq.

2002-06-19  David Aspinall  <da@proofgeneral.org>

	* generic/proof-menu.el:
	Match FSF C-button3 binding with XEmacs one

	* generic/proof-config.el:
	Doc improvements

2002-06-19  Pierre Courtieu  <courtieu@lri.fr>

	* coq/coq-syntax.el:
	Finished updating the commands and tactic lists of coq-syntax.el.

	* coq/coq-syntax.el:
	updated the lists of commands and tactics in coq-syntax.el.

2002-06-19  David Aspinall  <da@proofgeneral.org>

	* coq/coq.el:
	Use coq-proof-mode-p instead of nesting depth test.  Attempt to track nesting depth (fails).

	* etc/coq/nested.v:
	Add nested section example to increase the horror.

	* etc/coq/nested.v:
	Added End for sections, and silly test

	* etc/debugging-tips.txt:
	Updated with more notes

	* coq/coq.el:
	Clean up: remove count-undos, comments, tweak coq-proof-mode-p.

	* ChangeLog: Updated.

	* generic/proof-shell.el:
	Add proof-shell-last-prompt.

	* doc/PG-adapting.texi:
	Add doc of proof-shell-last-prompt.

	* doc/ProofGeneral.texi: Fix info

	* etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el:
	Set version tag for new release.

2002-06-18  David Aspinall  <da@proofgeneral.org>

	* html/develdownload.php:
	Update Emacs versions

	* doc/ProofGeneral.texi:
	Add news for PG 3.4

	* doc/PG-adapting.texi:
	Update magic.  Document nested proof settings.

	* coq/coq.el:
	Removed lift-global stuff.  coq-find-and-forget: only undo undoable tactics.

	* generic/proof-script.el:
	Remove lift-global function.

	* generic/proof-config.el, generic/proof-script.el:
	Remove global testing and lift-global function; rename proof-nested-goals -> proof-nested-goals-history.

	* etc/coq/nested.v:
	Added some non-undoable tactics

2002-06-19  David Aspinall  <da@proofgeneral.org>

	* generic/proof-shell.el:
	Add proof-shell-last-prompt.

	* doc/PG-adapting.texi:
	Add doc of proof-shell-last-prompt.

	* doc/ProofGeneral.texi: Fix info

	* etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el:
	Set version tag for new release.

2002-06-18  David Aspinall  <da@proofgeneral.org>

	* html/develdownload.php:
	Update Emacs versions

	* doc/ProofGeneral.texi:
	Add news for PG 3.4

	* doc/PG-adapting.texi:
	Update magic.  Document nested proof settings.

	* coq/coq.el:
	Removed lift-global stuff.  coq-find-and-forget: only undo undoable tactics.

	* generic/proof-script.el:
	Remove lift-global function.

	* generic/proof-config.el, generic/proof-script.el:
	Remove global testing and lift-global function; rename proof-nested-goals -> proof-nested-goals-history.

	* etc/coq/nested.v:
	Added some non-undoable tactics

	* etc/coq/nested.v: Added some sections

	* html/news.html, html/oldnews.html:
	News item for PG 3.4

2002-06-18  Pierre Courtieu  <courtieu@lri.fr>

	* coq/coq.el, coq/coq-syntax.el:
	Added the backtrack mechanism for sections. Seems to work.

	* coq/coq.el, coq/coq-syntax.el:
	Added a function to inspect the prompt of Coq, in order to know if we
	are in proof-mode. Redundant with proof-nesting-depth.

2002-06-18  David Aspinall  <da@proofgeneral.org>

	* coq/coq.el:
	Attempt at (alledgedly) more robust solution to find-and-forget.

	* etc/coq/nested.v: Fix

	* etc/coq/nested.v:
	Add more declarations

	* coq/coq.el:
	Test using proof-nesting-depth before calling Reset

2002-06-14  Pierre Courtieu  <courtieu@lri.fr>

	* coq/coq.el: Minor changes.

	* coq/coq.el:
	Print and Check guess their argument from the region or the string
	near the point.

2002-06-13  David Aspinall  <da@proofgeneral.org>

	* coq/coq.el:
	Disable count-undos function, just use find-and-forget.

	* generic/proof-script.el:
	A nil setting of proof-kill-goal-command forces use of proof-find-and-forget for all retraction.

	* generic/proof-config.el: Docs

	* generic/proof-shell.el:
	Experiment with showing real prover output for aborted proofs.

2002-06-12  David Aspinall  <da@proofgeneral.org>

	* coq/coq.el:
	Revised find-and-forget function, which also works for count-undos.

	* etc/coq/nested.v:
	More test cases, summary of situation.

	* generic/span-overlay.el:
	Second variant of next-span, without doubly nested loop

	* generic/span-overlay.el:
	Improve imp of next-span

	* etc/coq/nested.v: Note of another bug

	* coq/coq.el:
	Test for find-and-forget using Back always instead of Reset.

	* etc/coq/nested.v:
	Add test t4 for extra depth of nesting

	* generic/proof-utils.el:
	Make hack for XEmacs 21.4 also work for later versions

2002-06-12  Pierre Courtieu  <courtieu@lri.fr>

	* CHANGES:
	Changed the CHANGES file for Coq.

	* coq/coq.el:
	Nested proofs in Coq are well backtracked! I used the new field
	'nestedundos created by David. Will change the CHANGE file
	accordingly.

2002-06-12  David Aspinall  <da@proofgeneral.org>

	* generic/proof-script.el:
	Adjust proof-nesting depth, add FIXME notes since not right yet

	* isar/test.el: New files.

	* coq/coq.el:
	Add proof-nested-undo-regexp setting

	* generic/proof-script.el, generic/proof-config.el:
	Add nestedundos setting to span, and proof-nested-undo-regexp setting

2002-06-11  David Aspinall  <da@proofgeneral.org>

	* etc/coq/nested.v:
	Replace with example from Pierre

	* generic/proof-script.el:
	Only match saves for prover that supports nested proofs (restores old behaviour for Isar).  Isar goal/save regexps dont match up properly.

2002-06-11  Pierre Courtieu  <courtieu@lri.fr>

	* CHANGES: Not important.

	* CHANGES:
	CHANGE is cleaner in the Coq part! Not important.

	* CHANGES:
	Added changes in CHANGE about my new customization variables
	coq-user-backable-command etc.

	* coq/coq.el, coq/coq-syntax.el:
	Added the coq-user-... elisp customization variables to allow the user
	to defclare new commands and tactics:  must typically be customized in
	.emacs.

2002-06-11  David Aspinall  <da@proofgeneral.org>

	* coq/coq.el:
	Remove proof-nested-goals-p setting

	* generic/proof-script.el:
	Improved proof-nesting-depth (not finished yet)

2002-06-11  Pierre Courtieu  <courtieu@lri.fr>

	* coq/coq.el:
	Fixed a bug of the new synchro code (coq-find-and-forget) in
	coq.el. Now do not count Tactics and unsaved goal commands for "Back".

2002-06-11  David Aspinall  <da@proofgeneral.org>

	* generic/proof-config.el, generic/proof-shell.el, generic/proof-script.el:
	Add proof-nesting-depth, new implementation of span amalgamation in proof-done-advancing.

	* coq/coq.el:
	Set nested goals; include Lemma again in def of goal.

	* etc/coq/nested.v: New files.

2002-06-08  David Aspinall  <da@proofgeneral.org>

	* html/download.html:
	Mention not  supporting  E21

	* ChangeLog: Updated.

	* etc/ProofGeneral.spec:
	Add install for isartags

	* ChangeLog: Updated.

	* isar/isar.el:
	Fix bug in string syntax in isar-strip-terminators: did this work correctly before?

	* generic/span.el:
	Clean up span.el loading; make compat with bbdb.el in FSF

	* generic/proof-shell.el:
	Clean up span.el loading

	* ChangeLog: Updated.

	* todo: Updates

	* acl2/example.acl2: Remove duplicate

	* etc/ProofGeneral.spec: Add isartags

	* isar/isartags: Program [broken]

	* doc/ProofGeneral.texi: Update magic

	* coq/coqtags, lego/legotags:
	Default to /usr/bin/perl

	* CHANGES: Note about removing dirs

	* html/projects.html:
	Remove PGK mention, other obs projects

	* ChangeLog: Updated.

	* generic/proof-script.el:
	Robustness fixes/bug notes

	* generic/proof-menu.el: Spacing

	* generic/span-extent.el:
	Tweak liveness test

	* generic/proof-site.el: Alter order

	* generic/proof-config.el:
	Fix keysym to use FSF syntax

	* etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el:
	Set version tag for new release.

2002-06-08  David Aspinall  <da@proofgeneral.org>

	* etc/ProofGeneral.spec:
	Add install for isartags

	* ChangeLog: Updated.

	* isar/isar.el:
	Fix bug in string syntax in isar-strip-terminators: did this work correctly before?

	* generic/span.el:
	Clean up span.el loading; make compat with bbdb.el in FSF

	* generic/proof-shell.el:
	Clean up span.el loading

	* ChangeLog: Updated.

	* todo: Updates

	* acl2/example.acl2: Remove duplicate

	* etc/ProofGeneral.spec: Add isartags

	* isar/isartags: Program [broken]

	* doc/ProofGeneral.texi: Update magic

	* coq/coqtags, lego/legotags:
	Default to /usr/bin/perl

	* CHANGES: Note about removing dirs

	* html/projects.html:
	Remove PGK mention, other obs projects

	* ChangeLog: Updated.

	* generic/proof-script.el:
	Robustness fixes/bug notes

	* generic/proof-menu.el: Spacing

	* generic/span-extent.el:
	Tweak liveness test

	* generic/proof-site.el: Alter order

	* generic/proof-config.el:
	Fix keysym to use FSF syntax

	* etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el:
	Set version tag for new release.

2002-06-08  David Aspinall  <da@proofgeneral.org>

	* isar/isar.el:
	Fix bug in string syntax in isar-strip-terminators: did this work correctly before?

	* generic/span.el:
	Clean up span.el loading; make compat with bbdb.el in FSF

	* generic/proof-shell.el:
	Clean up span.el loading

	* ChangeLog: Updated.

	* todo: Updates

	* acl2/example.acl2: Remove duplicate

	* etc/ProofGeneral.spec: Add isartags

	* isar/isartags: Program [broken]

	* doc/ProofGeneral.texi: Update magic

	* coq/coqtags, lego/legotags:
	Default to /usr/bin/perl

	* CHANGES: Note about removing dirs

	* html/projects.html:
	Remove PGK mention, other obs projects

	* ChangeLog: Updated.

	* generic/proof-script.el:
	Robustness fixes/bug notes

	* generic/proof-menu.el: Spacing

	* generic/span-extent.el:
	Tweak liveness test

	* generic/proof-site.el: Alter order

	* generic/proof-config.el:
	Fix keysym to use FSF syntax

	* etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el:
	Set version tag for new release.

2002-06-08  David Aspinall  <da@proofgeneral.org>

	* todo: Updates

	* acl2/example.acl2: Remove duplicate

	* etc/ProofGeneral.spec: Add isartags

	* isar/isartags: Program [broken]

	* doc/ProofGeneral.texi: Update magic

	* coq/coqtags, lego/legotags:
	Default to /usr/bin/perl

	* CHANGES: Note about removing dirs

	* html/projects.html:
	Remove PGK mention, other obs projects

	* ChangeLog: Updated.

	* generic/proof-script.el:
	Robustness fixes/bug notes

	* generic/proof-menu.el: Spacing

	* generic/span-extent.el:
	Tweak liveness test

	* generic/proof-site.el: Alter order

	* generic/proof-config.el:
	Fix keysym to use FSF syntax

	* etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el:
	Set version tag for new release.

2002-06-08  David Aspinall  <da@proofgeneral.org>

	* generic/proof-script.el:
	Robustness fixes/bug notes

	* generic/proof-menu.el: Spacing

	* generic/span-extent.el:
	Tweak liveness test

	* generic/proof-site.el: Alter order

	* generic/proof-config.el:
	Fix keysym to use FSF syntax

	* etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el:
	Set version tag for new release.

2002-06-05  David Aspinall  <da@proofgeneral.org>

	* isar/isar-keywords.el:
	Add types_code and friends

2002-05-29  Pierre Courtieu  <courtieu@lri.fr>

	* coq/coq.el:
	Made a negative test to compute the number of "Back n" in
	coq-find-and-forget.

	* coq/coq.el, coq/coq-syntax.el:
	Modification of the coq-find-and-forget  function, in order to use the
	new "Back n." command of coq  to make the syncronization better. Seems
	to work, need to test.

	* coq/coq-syntax.el:
	Added some new tactic names

2002-05-21  David Aspinall  <da@proofgeneral.org>

	* isa/isabelle-system.el:
	Mistake in function name (Norbert Voelker <norbert@essex.ac.uk>)

2002-05-13  Markus Wenzel  <wenzelm@informatik.tu-muenchen.de>

	* doc/ProofGeneral.texi:
	updated URLxsymbol (unused);

2002-05-10  Markus Wenzel  <wenzelm@informatik.tu-muenchen.de>

	* isar/isar.el:
	tuned isar-strip-terminators;

2002-05-03  Markus Wenzel  <wenzelm@informatik.tu-muenchen.de>

	* TODO: fixed spelling;

	* isar/isar.el: tuned comment;

	* isar/todo, isar/isar.el:
	tuned proof-next-error setup;

2002-05-03  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.

	* html/eproofe.php, html/eproofe:
	New files.

	* generic/proof-x-symbol.el:
	Fix X-symbol URL

	* generic/proof-utils.el:
	Fix font lock for E21 (I hope)

	* generic/proof-config.el:
	Try to support next-error key binding for both Emacs versions.

	* doc/ProofGeneral.texi:
	Reflect change in load order

	* CHANGES: Updates

	* generic/proof-site.el:
	Fix loading order to load Isar before Isa

	* isar/isar.el:
	Added support for proof-shell-next-error

	* isar/isar.el:
	Add support for proof-next-error.

	* generic/proof-config.el:
	Craftily set experimental fetures on for devel release.

	* generic/pg-user.el:
	Began adding generic line-width adjust

2002-05-03  David Aspinall  <da@proofgeneral.org>

	* etc/ProofGeneral.spec, html/devel.html, generic/proof-site.el, html/develdownload.php:
	Set version tag for new release.

	* html/eproofe.php, html/eproofe:
	New files.

	* generic/proof-x-symbol.el:
	Fix X-symbol URL

	* generic/proof-utils.el:
	Fix font lock for E21 (I hope)

	* generic/proof-config.el:
	Try to support next-error key binding for both Emacs versions.

	* doc/ProofGeneral.texi:
	Reflect change in load order

	* CHANGES: Updates

	* generic/proof-site.el:
	Fix loading order to load Isar before Isa

	* isar/isar.el:
	Added support for proof-shell-next-error

	* isar/isar.el:
	Add support for proof-next-error.

	* generic/proof-config.el:
	Craftily set experimental fetures on for devel release.

	* generic/pg-user.el:
	Began adding generic line-width adjust

2002-04-24  David Aspinall  <da@proofgeneral.org>

	* CHANGES: Remove indents

	* isa/isa-syntax.el:
	Updated list of SML keywords

2002-04-23  David Aspinall  <da@proofgeneral.org>

	* ChangeLog: Updated.

	* etc/ProofGeneral.spec, generic/proof-site.el, html/develdownload.php, html/devel.html:
	Set version tag for new release.

	* doc/ProofGeneral.texi, doc/PG-adapting.texi, html/projects.html, html/screenshot.html, html/download.html, html/features.html, html/oldnews.html:
	Fix URL for X-symbol

	* todo: Updated

	* CHANGES:
	Add syntax highlighting cahanges from Lucas Dixon

	* isa/isa.el:
	Fix for E21 with isa-pre-shell-start.

	* isa/isa-syntax.el:
	Add syntax highlighting cahanges from Lucas Dixon

2002-04-23  David Aspinall  <da@proofgeneral.org>

	* etc/ProofGeneral.spec, generic/proof-site.el, html/develdownload.php, html/devel.html:
	Set version tag for new release.

	* doc/ProofGeneral.texi, doc/PG-adapting.texi, html/projects.html, html/screenshot.html, html/download.html, html/features.html, html/oldnews.html:
	Fix URL for X-symbol

	* todo: Updated

	* CHANGES:
	Add syntax highlighting cahanges from Lucas Dixon

	* isa/isa.el:
	Fix for E21 with isa-pre-shell-start.

	* isa/isa-syntax.el:
	Add syntax highlighting cahanges from Lucas Dixon

2002-03-22  David Aspinall  <da@proofgeneral.org>

	* ChangeLog: Updated.

	* etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el:
	Set version tag for new release.

2002-03-22  David Aspinall  <da@proofgeneral.org>

	* ChangeLog: Updated.

	* etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el:
	Set version tag for new release.

2002-03-22  David Aspinall  <da@proofgeneral.org>

	* etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el:
	Set version tag for new release.

2002-03-21  Christophe Raffalli  <Christophe.Raffalli@univ-savoie.fr>

	* phox/phox-font.el:
	*** empty log message ***

2002-03-21  David Aspinall  <da@proofgeneral.org>

	* ChangeLog: Updated.

	* CHANGES: Improvement to ACL2

	* acl2/acl2.el:
	Greatly improved support.

	* html/download.html: Typo

	* html/develdownload.php:
	No longer recommend XEmacs exclusively.

	* html/oldrel.php: FSF -> GNU

	* ChangeLog: Updated.

	* etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el:
	Set version tag for new release.

	* Makefile.devel:
	Revert accidental commit by crr

	* CHANGES: Updated.

	* generic/proof.el, generic/proof-toolbar.el, generic/proof-utils.el, generic/pg-pgip.el, generic/pg-user.el, generic/proof-depends.el, generic/proof-easy-config.el, generic/proof-splash.el, generic/pg-metadata.el:
	Year changes

	* generic/proof-shell.el:
	Remove toolbar gutters in multiple frame mode.  Add proof-shell-truncate-before-error setting.

	* generic/proof-script.el:
	Dont set type property for proof elements (experiment).  Tweak name determination/reporting.   Provide generic implementation of find-and-forget. Dont warn about some unnecessary settings

	* generic/proof-menu.el:
	Added activations for frame/window controls.

	* generic/proof-config.el:
	Added proof-shell-truncate-before-error, adjusted proof-toolbar-entries-default.

	* generic/proof-compat.el:
	Added emultation of display-graphic-p for XEmacs

	* generic/pg-xml.el:
	Add header to XML docs

	* generic/pg-xhtml.el: New files.

	* doc/PG-adapting.texi:
	Document some new settings

2002-03-21  Christophe Raffalli  <Christophe.Raffalli@univ-savoie.fr>

	* phox/phox.el, phox/x-symbol-phox.el, generic/proof-config.el, generic/proof-utils.el, phox/phox-font.el, Makefile.devel:
	added hook: proof-before-fontify-output-hook

2002-03-21  David Aspinall  <da@proofgeneral.org>

	* CHANGES: Improvement to ACL2

	* acl2/acl2.el:
	Greatly improved support.

	* html/download.html: Typo

	* html/develdownload.php:
	No longer recommend XEmacs exclusively.

	* html/oldrel.php: FSF -> GNU

	* ChangeLog: Updated.

	* etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el:
	Set version tag for new release.

	* Makefile.devel:
	Revert accidental commit by crr

	* CHANGES: Updated.

	* generic/proof.el, generic/proof-toolbar.el, generic/proof-utils.el, generic/pg-pgip.el, generic/pg-user.el, generic/proof-depends.el, generic/proof-easy-config.el, generic/proof-splash.el, generic/pg-metadata.el:
	Year changes

	* generic/proof-shell.el:
	Remove toolbar gutters in multiple frame mode.  Add proof-shell-truncate-before-error setting.

	* generic/proof-script.el:
	Dont set type property for proof elements (experiment).  Tweak name determination/reporting.   Provide generic implementation of find-and-forget. Dont warn about some unnecessary settings

	* generic/proof-menu.el:
	Added activations for frame/window controls.

	* generic/proof-config.el:
	Added proof-shell-truncate-before-error, adjusted proof-toolbar-entries-default.

	* generic/proof-compat.el:
	Added emultation of display-graphic-p for XEmacs

	* generic/pg-xml.el:
	Add header to XML docs

	* generic/pg-xhtml.el: New files.

	* doc/PG-adapting.texi:
	Document some new settings

2002-03-21  Christophe Raffalli  <Christophe.Raffalli@univ-savoie.fr>

	* phox/phox.el, phox/x-symbol-phox.el, generic/proof-config.el, generic/proof-utils.el, phox/phox-font.el, Makefile.devel:
	added hook: proof-before-fontify-output-hook

2002-03-21  David Aspinall  <da@proofgeneral.org>

	* etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el:
	Set version tag for new release.

	* Makefile.devel:
	Revert accidental commit by crr

	* CHANGES: Updated.

	* generic/proof.el, generic/proof-toolbar.el, generic/proof-utils.el, generic/pg-pgip.el, generic/pg-user.el, generic/proof-depends.el, generic/proof-easy-config.el, generic/proof-splash.el, generic/pg-metadata.el:
	Year changes

	* generic/proof-shell.el:
	Remove toolbar gutters in multiple frame mode.  Add proof-shell-truncate-before-error setting.

	* generic/proof-script.el:
	Dont set type property for proof elements (experiment).  Tweak name determination/reporting.   Provide generic implementation of find-and-forget. Dont warn about some unnecessary settings

	* generic/proof-menu.el:
	Added activations for frame/window controls.

	* generic/proof-config.el:
	Added proof-shell-truncate-before-error, adjusted proof-toolbar-entries-default.

	* generic/proof-compat.el:
	Added emultation of display-graphic-p for XEmacs

	* generic/pg-xml.el:
	Add header to XML docs

	* generic/pg-xhtml.el: New files.

	* doc/PG-adapting.texi:
	Document some new settings

2002-03-21  Christophe Raffalli  <Christophe.Raffalli@univ-savoie.fr>

	* phox/phox.el, phox/x-symbol-phox.el, generic/proof-config.el, generic/proof-utils.el, phox/phox-font.el, Makefile.devel:
	added hook: proof-before-fontify-output-hook

2002-03-05  Christophe Raffalli  <Christophe.Raffalli@univ-savoie.fr>

	* phox/phox.el, phox/phox-sym-lock.el, phox/README, phox/x-symbol-phox.el:
	*** empty log message ***

2002-02-23  David Aspinall  <da@proofgeneral.org>

	* generic/proof-shell.el:
	Add check for Emacs21.

	* generic/pg-user.el:
	Bug fix in proof-goto-command-end.  Decode x-syms in pg-insert-output-as-comment.

	* generic/proof-x-symbol.el:
	Simplify enabling tests to just check window-system.  Fix proof-x-symbol-decode-region to return new END value after decoding.

	* generic/proof-utils.el:
	Updates to font-lock handling in proof-fontify-region, proof-font-lock-clear-font-lock-vars.  Fix final return value in fontify region.

	* CHANGES: Update X-Sym status

2002-02-14  David Aspinall  <da@proofgeneral.org>

	* Makefile.devel:
	Remove latest-src-rpm link

	* ChangeLog: Updated.

	* etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el:
	Set version tag for new release.

2002-02-14  David Aspinall  <da@proofgeneral.org>

	* etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el:
	Set version tag for new release.

2002-02-12  Markus Wenzel  <wenzelm@informatik.tu-muenchen.de>

	* isar/interface, isa/interface:
	option -g GEOMETRY;

	* isar/isar.el:
	observe isar-undo-ignore-regexp in isar-count-undos and isar-find-and-forget;

	* isar/isar-syntax.el:
	added isar-undo-ignore-regexp;

2002-02-08  Markus Wenzel  <wenzelm@informatik.tu-muenchen.de>

	* isar/isar.el:
	more robust proof-shell-interrupt-regexp and proof-shell-error-regexp;

2002-01-31  David Aspinall  <da@proofgeneral.org>

	* ChangeLog: Updated.

	* html/about.html:
	Fix more broken front page links

	* INSTALL: Update for recent releases.

	* ChangeLog: Updated.

	* generic/proof-script.el:
	Simplify fix for repeated comments (commentre includes whitespace).

	* ChangeLog: Updated.

	* etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el:
	Set version tag for new release.

	* generic/proof-syntax.el:
	Tweak comment

	* generic/proof-script.el:
	Fix problem noticed with Isar and repeated comments.

	* etc/isar/CommentParsingBug.thy:
	New files.

2002-01-31  David Aspinall  <da@proofgeneral.org>

	* html/about.html:
	Fix more broken front page links

	* INSTALL: Update for recent releases.

	* ChangeLog: Updated.

	* generic/proof-script.el:
	Simplify fix for repeated comments (commentre includes whitespace).

	* ChangeLog: Updated.

	* etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el:
	Set version tag for new release.

	* generic/proof-syntax.el:
	Tweak comment

	* generic/proof-script.el:
	Fix problem noticed with Isar and repeated comments.

	* etc/isar/CommentParsingBug.thy:
	New files.

2002-01-31  David Aspinall  <da@proofgeneral.org>

	* generic/proof-script.el:
	Simplify fix for repeated comments (commentre includes whitespace).

	* ChangeLog: Updated.

	* etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el:
	Set version tag for new release.

	* generic/proof-syntax.el:
	Tweak comment

	* generic/proof-script.el:
	Fix problem noticed with Isar and repeated comments.

	* etc/isar/CommentParsingBug.thy:
	New files.

2002-01-31  David Aspinall  <da@proofgeneral.org>

	* etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el:
	Set version tag for new release.

	* generic/proof-syntax.el:
	Tweak comment

	* generic/proof-script.el:
	Fix problem noticed with Isar and repeated comments.

	* etc/isar/CommentParsingBug.thy:
	New files.

2002-01-26  Markus Wenzel  <wenzelm@informatik.tu-muenchen.de>

	* isar/isar-keywords.el: tuned comment;

2002-01-21  Markus Wenzel  <wenzelm@informatik.tu-muenchen.de>

	* isa/isabelle-system.el:
	full-proofs setting;

	* isa/README, isar/README:
	Isabelle2002 instead of Isabelle2001;

2002-01-17  Christophe Raffalli  <Christophe.Raffalli@univ-savoie.fr>

	* phox/.cvsignore:
	*** empty log message ***

2002-01-16  David Aspinall  <da@proofgeneral.org>

	* ChangeLog: Updated.

	* etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el:
	Set version tag for new release.

	* lego/example.l, isar/Example.thy, coq/example.v:
	Whitespace

	* generic/proof.el: Comments

	* generic/proof-script.el:
	Also bury trace buffer

	* generic/proof-config.el: Comments

	* isa/Example.ML: Whitespace

	* generic/proof-shell.el:
	Only create trace buffer if liable to be used.  Remove experimental spill-output style tracing code.

	* generic/proof-config.el, isar/isar.el, isa/isa.el:
	Set proof-shell-trace-output-regexp in proof-pre-shell-start-hook

	* isa/isa.el, isar/isar.el, generic/proof-config.el:
	Rename proof-shell-spill-output-regexp -> proof-shell-trace-output-regexp

	* doc/PG-adapting.texi:
	FSF Emacs -> GNU Emacs

	* doc/ProofGeneral.texi:
	Document the tracing buffer; FSF Emacs -> GNU Emacs

2002-01-16  David Aspinall  <da@proofgeneral.org>

	* etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el:
	Set version tag for new release.

	* lego/example.l, isar/Example.thy, coq/example.v:
	Whitespace

	* generic/proof.el: Comments

	* generic/proof-script.el:
	Also bury trace buffer

	* generic/proof-config.el: Comments

	* isa/Example.ML: Whitespace

	* generic/proof-shell.el:
	Only create trace buffer if liable to be used.  Remove experimental spill-output style tracing code.

	* generic/proof-config.el, isar/isar.el, isa/isa.el:
	Set proof-shell-trace-output-regexp in proof-pre-shell-start-hook

	* isa/isa.el, isar/isar.el, generic/proof-config.el:
	Rename proof-shell-spill-output-regexp -> proof-shell-trace-output-regexp

	* doc/PG-adapting.texi:
	FSF Emacs -> GNU Emacs

	* doc/ProofGeneral.texi:
	Document the tracing buffer; FSF Emacs -> GNU Emacs

2002-01-15  David Aspinall  <da@proofgeneral.org>

	* generic/proof-x-symbol.el:
	Also put trace buffer in x sym mode

	* ChangeLog: Updated.

	* generic/proof-shell.el:
	Remove defunct code

	* etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el:
	Set version tag for new release.

	* html/feedback.html: Deleted files.

	* CHANGES:
	Describe tracing improvements.

	* generic/proof-utils.el:
	windows-of-buffer -> get-buffer-window-list GNU name

	* generic/proof-shell.el:
	Inspect quit-flag when displaying tracing output; send an interrupt to the prover if set.

	* generic/proof-shell.el:
	Redisplay during tracing output on XEmacs

	* html/projects.html, html/download.html, html/gallery.php, html/links.html, html/main.html, html/oldnews.html:
	Fix link to feedback page

2002-01-15  David Aspinall  <da@proofgeneral.org>

	* generic/proof-shell.el:
	Remove defunct code

	* etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el:
	Set version tag for new release.

	* html/feedback.html: Deleted files.

	* CHANGES:
	Describe tracing improvements.

	* generic/proof-utils.el:
	windows-of-buffer -> get-buffer-window-list GNU name

	* generic/proof-shell.el:
	Inspect quit-flag when displaying tracing output; send an interrupt to the prover if set.

	* generic/proof-shell.el:
	Redisplay during tracing output on XEmacs

	* html/projects.html, html/download.html, html/gallery.php, html/links.html, html/main.html, html/oldnews.html:
	Fix link to feedback page

2002-01-14  Markus Wenzel  <wenzelm@informatik.tu-muenchen.de>

	* etc/isar/trace_simp.thy: tuned;

	* etc/isar/trace_simp.thy:
	some test cases for trace_simp output;

2002-01-11  David Aspinall  <da@proofgeneral.org>

	* COPYING: Fix numbering

	* CHANGES: Fix number

	* ChangeLog: Updated.

	* etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el:
	Set version tag for new release.

2002-01-11  David Aspinall  <da@proofgeneral.org>

	* etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el:
	Set version tag for new release.

2001-12-27  Markus Wenzel  <wenzelm@informatik.tu-muenchen.de>

	* isar/Example.thy: tuned;

	* isa/isabelle-system.el:
	trace_rules flag;

	* isar/BUGS, isa/README, isar/README, isar/todo:
	updated;

	* generic/README: fixed spelling;

2001-12-21  Markus Wenzel  <wenzelm@informatik.tu-muenchen.de>

	* isar/isar.el:
	do not set proof-shell-quit-cmd (admits persistent sessions);

2001-12-12  Markus Wenzel  <wenzelm@informatik.tu-muenchen.de>

	* isar/interface, isa/interface:
	incorporate smart X11 font installation (used to be in isatool installfonts);

2001-12-11  David Aspinall  <da@proofgeneral.org>

	* ChangeLog: Updated.

	* html/develdownload.php, html/main.html:
	Be politically correct about FSF GNU Emacs; update to mention version 21.

	* html/news.html, html/oldnews.html:
	fix links to devel download.

	* ChangeLog: Updated.

	* html/news.html:
	News item about Emacs 21 support

	* ChangeLog: Updated.

	* etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el:
	Set version tag for new release.

	* CHANGES:
	Note about Emacs 21 support and font lock.

	* generic/proof-utils.el:
	Protect XEmacs only code

	* generic/proof-site.el:
	Fix test for GNU 21

	* generic/proof-script.el:
	Change to font-lock support routines.

	* generic/proof-menu.el:
	Disable customize-menu-create for Emacs 21.

	* generic/proof-utils.el:
	Rework font-lock variable munging to work in GNU Emacs 21 also.

	* generic/proof-shell.el: Missing paren

	* generic/proof-config.el:
	Remove double setting, leave test setting in.

	* generic/proof-shell.el:
	Simplify -goals-config-done and -response-config-done to use current buffer.  Kill trace buffer with other associated buffers, and set specifiers similarly for multiple frames.

	* generic/proof-config.el:
	Added proof-trace-output-fontify-enable

	* CHANGES: Note of Emacs 21 support

	* generic/proof-toolbar.el:
	Add support for toolbars on Emacs 21.

	* generic/proof-splash.el:
	Add support for Emacs 21 image display.

	* generic/proof-site.el:
	Add proof-running-on-Emacs21 flag.

	* generic/proof-menu.el:
	Allow toolbar toggle for GNU Emacs 21.

	* html/features.html, generic/proof-config.el:
	Toolbar allowed in GNU Emacs 21

	* generic/proof-compat.el:
	Add proof-emacs-imagep function for GNU Emacs 21.

2001-12-11  David Aspinall  <da@proofgeneral.org>

	* html/develdownload.php, html/main.html:
	Be politically correct about FSF GNU Emacs; update to mention version 21.

	* html/news.html, html/oldnews.html:
	fix links to devel download.

	* ChangeLog: Updated.

	* html/news.html:
	News item about Emacs 21 support

	* ChangeLog: Updated.

	* etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el:
	Set version tag for new release.

	* CHANGES:
	Note about Emacs 21 support and font lock.

	* generic/proof-utils.el:
	Protect XEmacs only code

	* generic/proof-site.el:
	Fix test for GNU 21

	* generic/proof-script.el:
	Change to font-lock support routines.

	* generic/proof-menu.el:
	Disable customize-menu-create for Emacs 21.

	* generic/proof-utils.el:
	Rework font-lock variable munging to work in GNU Emacs 21 also.

	* generic/proof-shell.el: Missing paren

	* generic/proof-config.el:
	Remove double setting, leave test setting in.

	* generic/proof-shell.el:
	Simplify -goals-config-done and -response-config-done to use current buffer.  Kill trace buffer with other associated buffers, and set specifiers similarly for multiple frames.

	* generic/proof-config.el:
	Added proof-trace-output-fontify-enable

	* CHANGES: Note of Emacs 21 support

	* generic/proof-toolbar.el:
	Add support for toolbars on Emacs 21.

	* generic/proof-splash.el:
	Add support for Emacs 21 image display.

	* generic/proof-site.el:
	Add proof-running-on-Emacs21 flag.

	* generic/proof-menu.el:
	Allow toolbar toggle for GNU Emacs 21.

	* html/features.html, generic/proof-config.el:
	Toolbar allowed in GNU Emacs 21

	* generic/proof-compat.el:
	Add proof-emacs-imagep function for GNU Emacs 21.

2001-12-11  David Aspinall  <da@proofgeneral.org>

	* html/news.html:
	News item about Emacs 21 support

	* ChangeLog: Updated.

	* etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el:
	Set version tag for new release.

	* CHANGES:
	Note about Emacs 21 support and font lock.

	* generic/proof-utils.el:
	Protect XEmacs only code

	* generic/proof-site.el:
	Fix test for GNU 21

	* generic/proof-script.el:
	Change to font-lock support routines.

	* generic/proof-menu.el:
	Disable customize-menu-create for Emacs 21.

	* generic/proof-utils.el:
	Rework font-lock variable munging to work in GNU Emacs 21 also.

	* generic/proof-shell.el: Missing paren

	* generic/proof-config.el:
	Remove double setting, leave test setting in.

	* generic/proof-shell.el:
	Simplify -goals-config-done and -response-config-done to use current buffer.  Kill trace buffer with other associated buffers, and set specifiers similarly for multiple frames.

	* generic/proof-config.el:
	Added proof-trace-output-fontify-enable

	* CHANGES: Note of Emacs 21 support

	* generic/proof-toolbar.el:
	Add support for toolbars on Emacs 21.

	* generic/proof-splash.el:
	Add support for Emacs 21 image display.

	* generic/proof-site.el:
	Add proof-running-on-Emacs21 flag.

	* generic/proof-menu.el:
	Allow toolbar toggle for GNU Emacs 21.

	* html/features.html, generic/proof-config.el:
	Toolbar allowed in GNU Emacs 21

	* generic/proof-compat.el:
	Add proof-emacs-imagep function for GNU Emacs 21.

2001-12-11  David Aspinall  <da@proofgeneral.org>

	* etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el:
	Set version tag for new release.

	* CHANGES:
	Note about Emacs 21 support and font lock.

	* generic/proof-utils.el:
	Protect XEmacs only code

	* generic/proof-site.el:
	Fix test for GNU 21

	* generic/proof-script.el:
	Change to font-lock support routines.

	* generic/proof-menu.el:
	Disable customize-menu-create for Emacs 21.

	* generic/proof-utils.el:
	Rework font-lock variable munging to work in GNU Emacs 21 also.

	* generic/proof-shell.el: Missing paren

	* generic/proof-config.el:
	Remove double setting, leave test setting in.

	* generic/proof-shell.el:
	Simplify -goals-config-done and -response-config-done to use current buffer.  Kill trace buffer with other associated buffers, and set specifiers similarly for multiple frames.

	* generic/proof-config.el:
	Added proof-trace-output-fontify-enable

	* CHANGES: Note of Emacs 21 support

	* generic/proof-toolbar.el:
	Add support for toolbars on Emacs 21.

	* generic/proof-splash.el:
	Add support for Emacs 21 image display.

	* generic/proof-site.el:
	Add proof-running-on-Emacs21 flag.

	* generic/proof-menu.el:
	Allow toolbar toggle for GNU Emacs 21.

	* html/features.html, generic/proof-config.el:
	Toolbar allowed in GNU Emacs 21

	* generic/proof-compat.el:
	Add proof-emacs-imagep function for GNU Emacs 21.

2001-12-10  David Aspinall  <da@proofgeneral.org>

	* generic/proof-utils.el, generic/proof-shell.el:
	Add handling of proof-trace-buffer.

	* generic/proof.el:
	Added proof-trace-buffer.

	* generic/proof-utils.el, generic/proof-shell.el:
	Dont return a fontified string in proof-response-buffer-display.

2001-12-05  Markus Wenzel  <wenzelm@informatik.tu-muenchen.de>

	* generic/proof-shell.el:
	proof-release-lock: do not touch proof-shell-spill-output-buffer;
	proof-shell-spill-output-begin: reuse existing buffer;

	* isar/isar.el:
	activate proof-shell-spill-output-regexp;

2001-12-04  David Aspinall  <da@proofgeneral.org>

	* ChangeLog: Updated.

	* etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el:
	Set version tag for new release.

	* CHANGES: Update for 3.4pre

	* html/devel.html:
	Update mailing list address (point to web page)

2001-12-04  Markus Wenzel  <wenzelm@informatik.tu-muenchen.de>

	* doc/PG-adapting.texi:
	update from make process;

	* doc/ProofGeneral.texi, isar/isar.el:
	isar specific commands for bold/sup/sub;

	* isa/x-symbol-isabelle.el:
	added symbols for alternative 0..9;

2001-12-04  David Aspinall  <da@proofgeneral.org>

	* etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el:
	Set version tag for new release.

	* CHANGES: Update for 3.4pre

	* html/devel.html:
	Update mailing list address (point to web page)

2001-12-04  Markus Wenzel  <wenzelm@informatik.tu-muenchen.de>

	* doc/PG-adapting.texi:
	update from make process;

	* doc/ProofGeneral.texi, isar/isar.el:
	isar specific commands for bold/sup/sub;

	* isa/x-symbol-isabelle.el:
	added symbols for alternative 0..9;

2001-12-01  Markus Wenzel  <wenzelm@informatik.tu-muenchen.de>

	* isa/x-symbol-isabelle.el:
	\<euro> symbol;
	use previously defined x-symbol-isabelle-user-table (or nil);
	x-symbol-user-table achieves electric |- and |= symbols;

2001-11-24  Markus Wenzel  <wenzelm@informatik.tu-muenchen.de>

	* isar/isar.el:
	proof-shell-spill-output-regexp temporarily disabled;

2001-11-20  Markus Wenzel  <wenzelm@informatik.tu-muenchen.de>

	* isar/isar.el:
	set proof-shell-spill-output-regexp;
	isar-activate-scripting: proof-syn-cd (why is this here needed?);

2001-11-13  Markus Wenzel  <wenzelm@informatik.tu-muenchen.de>

	* isa/interface, isar/interface:
	option -k for logic specific isar-keywords file;

2001-11-08  Markus Wenzel  <wenzelm@informatik.tu-muenchen.de>

	* isa/x-symbol-isabelle.el:
	added \<index> symbol;

2001-11-07  Markus Wenzel  <wenzelm@informatik.tu-muenchen.de>

	* isa/x-symbol-isabelle.el:
	added \<lozenge> and \<struct>;

	* isar/isar-syntax.el:
	updated isar-goals-font-lock-keywords;

2001-10-24  David Aspinall  <da@proofgeneral.org>

	* html/main.html:
	Fix missing arg to get.
	Add Paul Roziere as req'd by Christopphe Raffalli

2001-10-13  Markus Wenzel  <wenzelm@informatik.tu-muenchen.de>

	* isar/isar-syntax.el:
	isar-goals-font-lock-keywords: more general goal pattern;

2001-10-08  David Aspinall  <da@proofgeneral.org>

	* ChangeLog: Updated.

	* etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el:
	Set version tag for new release.

	* CHANGES: Add back note.

2001-10-08  David Aspinall  <da@proofgeneral.org>

	* etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el:
	Set version tag for new release.

	* CHANGES: Add back note.

2001-10-04  Markus Wenzel  <wenzelm@informatik.tu-muenchen.de>

	* isar/isar.el:
	added isar-help-induct-rules;

2001-10-04  David Aspinall  <da@proofgeneral.org>

	* CHANGES: Remove note for devel

	* generic/proof-toolbar.el:
	Fix fudged enabler to call button function interactively.

2001-09-26  Markus Wenzel  <wenzelm@informatik.tu-muenchen.de>

	* isa/x-symbol-isabelle.el:
	support \<^bold> control symbols;

	* generic/proof-config.el:
	fixed spelling;

2001-09-24  David Aspinall  <da@proofgeneral.org>

	* ChangeLog: Updated.

	* etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el:
	Set version tag for new release.

	* coq/coq.el:
	Add Lemma to exclusion for coq-goal-command-p.

	* doc/PG-adapting.texi: Update magic

	* doc/docstring-magic.el: New line

	* generic/proof-config.el:
	Fix error in docs of stop-silent-command, and name of pre-shell-start-hook.

	* doc/ProofGeneral.texi:
	Another bug reporter

	* generic/proof-shell.el:
	Implement Robert Schnecks idea to help Coq display whole of goals output.

	* CHANGES: Devel release is tweaked 3.3

2001-09-24  David Aspinall  <da@proofgeneral.org>

	* etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el:
	Set version tag for new release.

	* coq/coq.el:
	Add Lemma to exclusion for coq-goal-command-p.

	* doc/PG-adapting.texi: Update magic

	* doc/docstring-magic.el: New line

	* generic/proof-config.el:
	Fix error in docs of stop-silent-command, and name of pre-shell-start-hook.

	* doc/ProofGeneral.texi:
	Another bug reporter

	* generic/proof-shell.el:
	Implement Robert Schnecks idea to help Coq display whole of goals output.

	* CHANGES: Devel release is tweaked 3.3

2001-09-13  David Aspinall  <da@proofgeneral.org>

	* ChangeLog: Updated.

	* doc/PG-adapting.texi:
	Link uref nicely

	* doc/ProofGeneral.texi:
	Minor improvements

	* doc/ProofGeneral.texi:
	Updates from an old printout of the manual

	* todo: updated

	* doc/PG-adapting.texi:
	Updates from an old printout of the manual

	* ChangeLog: Updated.

	* html/Kit/Makefile: New files.

	* html/Kit/dtd/pgip.dtd, html/Kit/dtd/pgml.dtd:
	Updated from Kit repo

	* html/download.html: Fix link

	* html/smallpage.php:
	Fix two more gaping holes letting people examine whole filesystem (also fixed in server anyway)

	* html/feedback, html/feedback.html, html/develdownload, html/develdownload.html, html/kit.php, html/kit, html/kit.html:
	PHP in php, html and no extn link to php

	* ChangeLog: Updated.

	* html/htmlshow.php:
	Fix two more gaping holes letting people examine whole filesystem

	* ChangeLog: Updated.

	* etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el:
	Set version tag for new release.

	* html/feedback: Feedback quick link

	* CHANGES: No changes msg

	* html/kit.html, html/mailinglist.html, html/develdownload.html, html/doc.html, html/feedback.html, html/kit, html/.htaccess:
	Try to fix PHP/html nonsense, by disabling SSI and enabling php for .html files

2001-09-13  David Aspinall  <da@proofgeneral.org>

	* doc/PG-adapting.texi:
	Link uref nicely

	* doc/ProofGeneral.texi:
	Minor improvements

	* doc/ProofGeneral.texi:
	Updates from an old printout of the manual

	* todo: updated

	* doc/PG-adapting.texi:
	Updates from an old printout of the manual

	* ChangeLog: Updated.

	* html/Kit/Makefile: New files.

	* html/Kit/dtd/pgip.dtd, html/Kit/dtd/pgml.dtd:
	Updated from Kit repo

	* html/download.html: Fix link

	* html/smallpage.php:
	Fix two more gaping holes letting people examine whole filesystem (also fixed in server anyway)

	* html/feedback, html/feedback.html, html/develdownload, html/develdownload.html, html/kit.php, html/kit, html/kit.html:
	PHP in php, html and no extn link to php

	* ChangeLog: Updated.

	* html/htmlshow.php:
	Fix two more gaping holes letting people examine whole filesystem

	* ChangeLog: Updated.

	* etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el:
	Set version tag for new release.

	* html/feedback: Feedback quick link

	* CHANGES: No changes msg

	* html/kit.html, html/mailinglist.html, html/develdownload.html, html/doc.html, html/feedback.html, html/kit, html/.htaccess:
	Try to fix PHP/html nonsense, by disabling SSI and enabling php for .html files

2001-09-13  David Aspinall  <da@proofgeneral.org>

	* html/Kit/Makefile: New files.

	* html/Kit/dtd/pgip.dtd, html/Kit/dtd/pgml.dtd:
	Updated from Kit repo

	* html/download.html: Fix link

	* html/smallpage.php:
	Fix two more gaping holes letting people examine whole filesystem (also fixed in server anyway)

	* html/feedback, html/feedback.html, html/develdownload, html/develdownload.html, html/kit.php, html/kit, html/kit.html:
	PHP in php, html and no extn link to php

	* ChangeLog: Updated.

	* html/htmlshow.php:
	Fix two more gaping holes letting people examine whole filesystem

	* ChangeLog: Updated.

	* etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el:
	Set version tag for new release.

	* html/feedback: Feedback quick link

	* CHANGES: No changes msg

	* html/kit.html, html/mailinglist.html, html/develdownload.html, html/doc.html, html/feedback.html, html/kit, html/.htaccess:
	Try to fix PHP/html nonsense, by disabling SSI and enabling php for .html files

2001-09-13  David Aspinall  <da@proofgeneral.org>

	* html/htmlshow.php:
	Fix two more gaping holes letting people examine whole filesystem

	* ChangeLog: Updated.

	* etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el:
	Set version tag for new release.

	* html/feedback: Feedback quick link

	* CHANGES: No changes msg

	* html/kit.html, html/mailinglist.html, html/develdownload.html, html/doc.html, html/feedback.html, html/kit, html/.htaccess:
	Try to fix PHP/html nonsense, by disabling SSI and enabling php for .html files

2001-09-13  David Aspinall  <da@proofgeneral.org>

	* etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el:
	Set version tag for new release.

	* html/feedback: Feedback quick link

	* CHANGES: No changes msg

	* html/kit.html, html/mailinglist.html, html/develdownload.html, html/doc.html, html/feedback.html, html/kit, html/.htaccess:
	Try to fix PHP/html nonsense, by disabling SSI and enabling php for .html files

2001-09-10  David Aspinall  <da@proofgeneral.org>

	* ChangeLog: Updated.

	* etc/ProofGeneral.spec, generic/proof-site.el:
	Set version tag for new release.

	* etc/release-log.txt:
	Note about re-rel 3.3

	* html/download.html, html/news.html:
	Update release dates

	* todo: Update todo

	* doc/ProofGeneral.texi:
	Remove spurious comment at start

2001-09-10  Markus Wenzel  <wenzelm@informatik.tu-muenchen.de>

	* isar/isar-syntax.el:
	isar-goals-font-lock-keywords: corollary;

2001-09-10  David Aspinall  <da@proofgeneral.org>

	* etc/ProofGeneral.spec, generic/proof-site.el:
	Set version tag for new release.

	* etc/release-log.txt:
	Note about re-rel 3.3

	* html/download.html, html/news.html:
	Update release dates

	* todo: Update todo

	* doc/ProofGeneral.texi:
	Remove spurious comment at start

2001-09-10  Markus Wenzel  <wenzelm@informatik.tu-muenchen.de>

	* isar/isar-syntax.el:
	isar-goals-font-lock-keywords: corollary;

2001-09-09  David Aspinall  <da@proofgeneral.org>

	* ChangeLog: Updated.

	* etc/ProofGeneral.spec, generic/proof-site.el:
	Set version tag for new release.

	* ChangeLog: Updated.

	* html/hits, html/hits.html:
	Renamed file

	* Makefile.devel:
	Fixup copying of releasename link

	* ChangeLog: Updated.

	* etc/ProofGeneral.spec, generic/proof-site.el:
	Set version tag for new release.

	* Makefile.devel: Finished shift to 3.4

	* html/kit: Link to kit.php

	* html/kit.html, html/kit.php:
	File determination nonsense

	* html/download.html:
	Change over to some .php files.

	* CHANGES:
	Backtrack to previous CHANGES file for now.

	* coq/README, lego/README:
	Coq/lego confusion

	* coq/BUGS:
	Bug in new parsing for coq, mention

	* ChangeLog: Updated.

	* etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el:
	Set version tag for new release.

	* Makefile.devel: Update for 3.4pre

	* html/footer.html:
	Remove validation stamp from footer, since its a lie.

	* CHANGES: No changes yet

	* ChangeLog: Updated.

	* etc/ProofGeneral.spec, generic/proof-site.el:
	Set version tag for new release.

	* html/download.html: Trim page a bit

	* html/news.html, html/oldnews.html:
	Announce 3.3

	* html/doc.html: Release 3-3.

	* etc/release-log.txt:
	Release date of 3-3.

	* html/download.html:
	Mention paper letter registrations.

	* html/download.html:
	Remove to be released line

	* doc/PG-adapting.texi: Update docs.

2001-09-09  David Aspinall  <da@proofgeneral.org>

	* etc/ProofGeneral.spec, generic/proof-site.el:
	Set version tag for new release.

	* ChangeLog: Updated.

	* html/hits, html/hits.html:
	Renamed file

	* Makefile.devel:
	Fixup copying of releasename link

	* ChangeLog: Updated.

	* etc/ProofGeneral.spec, generic/proof-site.el:
	Set version tag for new release.

	* Makefile.devel: Finished shift to 3.4

	* html/kit: Link to kit.php

	* html/kit.html, html/kit.php:
	File determination nonsense

	* html/download.html:
	Change over to some .php files.

	* CHANGES:
	Backtrack to previous CHANGES file for now.

	* coq/README, lego/README:
	Coq/lego confusion

	* coq/BUGS:
	Bug in new parsing for coq, mention

	* ChangeLog: Updated.

	* etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el:
	Set version tag for new release.

	* Makefile.devel: Update for 3.4pre

	* html/footer.html:
	Remove validation stamp from footer, since its a lie.

	* CHANGES: No changes yet

	* ChangeLog: Updated.

	* etc/ProofGeneral.spec, generic/proof-site.el:
	Set version tag for new release.

	* html/download.html: Trim page a bit

	* html/news.html, html/oldnews.html:
	Announce 3.3

	* html/doc.html: Release 3-3.

	* etc/release-log.txt:
	Release date of 3-3.

	* html/download.html:
	Mention paper letter registrations.

	* html/download.html:
	Remove to be released line

	* doc/PG-adapting.texi: Update docs.

2001-09-09  David Aspinall  <da@proofgeneral.org>

	* html/hits, html/hits.html:
	Renamed file

	* Makefile.devel:
	Fixup copying of releasename link

	* ChangeLog: Updated.

	* etc/ProofGeneral.spec, generic/proof-site.el:
	Set version tag for new release.

	* Makefile.devel: Finished shift to 3.4

	* html/kit: Link to kit.php

	* html/kit.html, html/kit.php:
	File determination nonsense

	* html/download.html:
	Change over to some .php files.

	* CHANGES:
	Backtrack to previous CHANGES file for now.

	* coq/README, lego/README:
	Coq/lego confusion

	* coq/BUGS:
	Bug in new parsing for coq, mention

	* ChangeLog: Updated.

	* etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el:
	Set version tag for new release.

	* Makefile.devel: Update for 3.4pre

	* html/footer.html:
	Remove validation stamp from footer, since its a lie.

	* CHANGES: No changes yet

	* ChangeLog: Updated.

	* etc/ProofGeneral.spec, generic/proof-site.el:
	Set version tag for new release.

	* html/download.html: Trim page a bit

	* html/news.html, html/oldnews.html:
	Announce 3.3

	* html/doc.html: Release 3-3.

	* etc/release-log.txt:
	Release date of 3-3.

	* html/download.html:
	Mention paper letter registrations.

	* html/download.html:
	Remove to be released line

	* doc/PG-adapting.texi: Update docs.

2001-09-09  David Aspinall  <da@proofgeneral.org>

	* etc/ProofGeneral.spec, generic/proof-site.el:
	Set version tag for new release.

	* Makefile.devel: Finished shift to 3.4

	* html/kit: Link to kit.php

	* html/kit.html, html/kit.php:
	File determination nonsense

	* html/download.html:
	Change over to some .php files.

	* CHANGES:
	Backtrack to previous CHANGES file for now.

	* coq/README, lego/README:
	Coq/lego confusion

	* coq/BUGS:
	Bug in new parsing for coq, mention

	* ChangeLog: Updated.

	* etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el:
	Set version tag for new release.

	* Makefile.devel: Update for 3.4pre

	* html/footer.html:
	Remove validation stamp from footer, since its a lie.

	* CHANGES: No changes yet

	* ChangeLog: Updated.

	* etc/ProofGeneral.spec, generic/proof-site.el:
	Set version tag for new release.

	* html/download.html: Trim page a bit

	* html/news.html, html/oldnews.html:
	Announce 3.3

	* html/doc.html: Release 3-3.

	* etc/release-log.txt:
	Release date of 3-3.

	* html/download.html:
	Mention paper letter registrations.

	* html/download.html:
	Remove to be released line

	* doc/PG-adapting.texi: Update docs.

2001-09-09  David Aspinall  <da@proofgeneral.org>

	* etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el:
	Set version tag for new release.

	* Makefile.devel: Update for 3.4pre

	* html/footer.html:
	Remove validation stamp from footer, since its a lie.

	* CHANGES: No changes yet

	* ChangeLog: Updated.

	* etc/ProofGeneral.spec, generic/proof-site.el:
	Set version tag for new release.

	* html/download.html: Trim page a bit

	* html/news.html, html/oldnews.html:
	Announce 3.3

	* html/doc.html: Release 3-3.

	* etc/release-log.txt:
	Release date of 3-3.

	* html/download.html:
	Mention paper letter registrations.

	* html/download.html:
	Remove to be released line

	* doc/PG-adapting.texi: Update docs.

2001-09-09  David Aspinall  <da@proofgeneral.org>

	* etc/ProofGeneral.spec, generic/proof-site.el:
	Set version tag for new release.

	* html/download.html: Trim page a bit

	* html/news.html, html/oldnews.html:
	Announce 3.3

	* html/doc.html: Release 3-3.

	* etc/release-log.txt:
	Release date of 3-3.

	* html/download.html:
	Mention paper letter registrations.

	* html/download.html:
	Remove to be released line

	* doc/PG-adapting.texi: Update docs.

2001-09-06  Markus Wenzel  <wenzelm@informatik.tu-muenchen.de>

	* isa/interface, isar/interface:
	tuned usage;

2001-09-05  David Aspinall  <da@proofgeneral.org>

	* doc/ProofGeneral.texi:
	Mention pg-toggle-visibility and its keybinding

	* ChangeLog: Updated.

	* etc/ProofGeneral.spec, html/devel.html, generic/proof-site.el, html/develdownload.php:
	Set version tag for new release.

	* generic/pg-metadata.el: Incomplete

	* doc/ProofGeneral.texi: Todo

	* CHANGES, todo:
	Updated

	* generic/proof-menu.el:
	Add keybindings for new commands for moving/navigating spans.

	* generic/proof-script.el:
	Fix problem with C-x C-v by copying buffer-file-name. Add children property to control spans.

	* generic/pg-user.el:
	Improved span moving and navigation commands.

2001-09-05  David Aspinall  <da@proofgeneral.org>

	* etc/ProofGeneral.spec, html/devel.html, generic/proof-site.el, html/develdownload.php:
	Set version tag for new release.

	* generic/pg-metadata.el: Incomplete

	* doc/ProofGeneral.texi: Todo

	* CHANGES, todo:
	Updated

	* generic/proof-menu.el:
	Add keybindings for new commands for moving/navigating spans.

	* generic/proof-script.el:
	Fix problem with C-x C-v by copying buffer-file-name. Add children property to control spans.

	* generic/pg-user.el:
	Improved span moving and navigation commands.

2001-09-04  Markus Wenzel  <wenzelm@informatik.tu-muenchen.de>

	* isar/Example.thy: tuned proof text;
	added script version;

	* isa/interface, isar/interface:
	added option -P: actually start Proof General (default true);

2001-09-04  David Aspinall  <da@proofgeneral.org>

	* ChangeLog: Updated.

	* etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el:
	Set version tag for new release.

	* generic/pg-xml.el:
	Issue parsing messages

	* generic/pg-user.el:
	Add commands to move spans up/down.  Enable features only if experimental flag set

	* generic/proof-script.el:
	Nested proof spans are duplicable

	* generic/proof-config.el:
	Add experimental features setting

	* Makefile: Delete rogue elcs

	* CHANGES, INSTALL:
	Updates

2001-09-04  Markus Wenzel  <wenzelm@informatik.tu-muenchen.de>

	* isar/README: tuned;

	* isa/README, isar/README:
	no need to adjust the path to bash on the first line (due to /usr/bin/env);

2001-09-04  David Aspinall  <da@proofgeneral.org>

	* etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el:
	Set version tag for new release.

	* generic/pg-xml.el:
	Issue parsing messages

	* generic/pg-user.el:
	Add commands to move spans up/down.  Enable features only if experimental flag set

	* generic/proof-script.el:
	Nested proof spans are duplicable

	* generic/proof-config.el:
	Add experimental features setting

	* Makefile: Delete rogue elcs

	* CHANGES, INSTALL:
	Updates

2001-09-04  Markus Wenzel  <wenzelm@informatik.tu-muenchen.de>

	* isar/README: tuned;

	* isa/README, isar/README:
	no need to adjust the path to bash on the first line (due to /usr/bin/env);

2001-09-03  David Aspinall  <da@proofgeneral.org>

	* ChangeLog: Updated.

	* README.devel: Text

	* ChangeLog: Trim dups

	* README.windows: Add author

	* TODO, CHANGES:
	Updated

	* isa/Example.ML:
	Accidental commit; revert to original.

	* isar/isar.el:
	Set proof-goal-with-hole-regexp

	* generic/proof-config.el:
	Change colour of locked region.

	* generic/proof-shell.el:
	Fix bracket bug.

	* generic/proof-script.el:
	Show/hide all proofs: add redisplay for FSF
	Use new functions pg-set-span-helphighlights and pg-span-name
	to set help echo, balloon help, mouse highlight, and context
	menu.

	* generic/proof-depends.el:
	Use pg-set-span-helphightlights for unhighlighting.

	* generic/pg-user.el:
	Generalise context menu for other spans; grey out show/hide when unavailable.

	* html/main.html: Join paras

	* ChangeLog: Updated.

	* html/features.html: Text

	* html/features.html:
	Fix link to screenshot

	* html/doc.html: Improve layout

	* doc/PG-adapting.texi, doc/ProofGeneral.texi:
	Update version numbers, time stamps.

	* html/download.html:
	Typo.  Update Emacs version to 20.7.

	* ChangeLog: Updated.

	* html/oldrel.php: Update branch

	* html/download.html: PHP file

	* html/oldrel.html, html/oldrel.php:
	Renamed file

	* etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el:
	Set version tag for new release.

	* html/download.html:
	Please try devel version

	* bin/proofgeneral, demoisa/demoisa.el:
	Accidental update; revert to previous

	* demoisa/README: Rearrange

	* twelf/twelf.el, twelf/x-symbol-twelf.el, twelf/twelf-old.el, plastic/todo, twelf/example.elf, twelf/README, twelf/twelf-font.el, plastic/plastic.el, plastic/plastic-syntax.el, plastic/test.lf, phox/phox.el, plastic/README, phox/phox-outline.el, phox/phox-sym-lock.el, phox/phox-tags.el, phox/example.phx, phox/phox-extraction.el, phox/phox-font.el, phox/phox-fun.el, lego/readonly/readonly.l, papers/README, phox/README, lego/legotags, lego/todo, lego/x-symbol-lego.el, lego/example2.l, lego/lego.el, lego/lego-syntax.el, lego/BUGS, lego/example.l, lego/README, isar/todo, isar/isar.el, isar/isar-keywords.el, isar/isar-syntax.el, isar/BUGS, isar/Example.thy, isar/interface, isar/README, isa/todo, isa/x-symbol-isabelle.el, isa/isabelle-system.el, isa/thy-mode.el, isa/isa.el, isa/interface, isa/interface-setup.el, isa/isa-syntax.el, isa/depends.ML, isa/Example2.ML, isa/README, isa/BUGS, isa/Example.ML, isa/Example.thy, isa/Example-Xsym.ML, images/gimp/.cvsignore, images/gimp/scripts/proofgeneral.scm, images/use.8bit.xpm, images/use.xcf, images/use.xpm, images/undo.8bit.xpm, images/undo.xcf, images/undo.xpm, images/retract.xpm, images/state.8bit.xpm, images/state.xcf, images/state.xpm, images/restart.xpm, images/retract.8bit.xpm, images/retract.xcf, images/qed.xpm, images/restart.8bit.xpm, images/restart.xcf, images/pgicon.png, images/pgmini.xpm, images/qed.8bit.xpm, images/qed.xcf, images/pg-text.xcf, images/pg-text.8bit.gif, images/pg-text.gif, images/pg-text.jpg, images/next.xcf, images/next.xpm, images/notes.txt, images/next.8bit.xpm, images/lego-badge.xcf, images/isabelle_transparent.8bit.gif, images/isabelle_transparent.gif, images/isabelle_transparent.xcf, images/isabelle-badge.xcf, images/info.xpm, images/interrupt.8bit.xpm, images/interrupt.xcf, images/interrupt.xpm, images/help.xpm, images/info.8bit.xpm, images/info.xcf, images/goto.xcf, images/goto.xpm, images/help.8bit.xpm, images/help.xcf, images/goto.8bit.xpm, images/goal_large.xcf, images/goal.8bit.xpm, images/goal.xcf, images/goal.xpm, images/find.xpm, images/fireworks.xcf, images/find.8bit.xpm, images/find.xcf, images/context.xpm, images/coq-badge.xcf, images/command.xcf, images/command.xpm, images/context.8bit.xpm, images/context.xcf, images/abort.xpm, images/blank.xcf, images/command.8bit.xpm, images/abort.8bit.xpm, images/abort.xcf, images/README, images/ProofGeneral.jpg, images/ProofGeneral.xcf, images/ProofGeneral.8bit.gif, images/ProofGeneral.gif, images/.cvsignore, images/Makefile, html/projects/test.html, html/projects/thybrowse.html, html/projects/webreplay.html, html/projects/xmlpgip.html, html/projects/pgip.html, html/projects/pgml.html, html/projects/reelcase.html, html/projects/scrgen.html, html/projects/hol.html, html/projects/isapbp.html, html/projects/mm.html, html/projects/outline.html, html/projects/coqfile.html, html/projects/coqpbp.html, html/projects/corba.html, html/projects/acs.html, html/papers/pgtalk.pdf, html/papers/pgoutline.ps.gz, html/papers/pgoutline.pdf, html/images/whole-man.jpg, html/images/whole-man-thumb.jpg, html/images/silverrule.gif, html/images/vh40.gif, html/images/whip.jpg, html/images/whip-thumb.jpg, html/images/pg-text.gif, html/images/portrait.jpg, html/images/portrait-thumb.jpg, html/images/pg-lego-console.png, html/images/pg-lego-screenshot.png, html/images/pg-lego-thumb.png, html/images/pg-isar-thumb.png, html/images/pg-lego-console-thumb.png, html/images/pg-isar-screenshot.png, html/images/pg-isa-screenshot.png, html/images/pg-isa-thumb.png, html/images/pg-coq-thumb.png, html/images/isabelle.gif, html/images/lego-badge.gif, html/images/pg-coq-screenshot.png, html/images/canvaswallpaper.jpg, html/images/coq-badge.gif, html/images/coqlogo4.gif, html/images/coqlogo4.xcf, html/images/isabelle-badge.gif, html/images/bullethole.gif, html/images/PG-small.jpg, html/images/ProofGeneral.jpg, html/images/.cvsignore, html/images/IsaPGscreen.jpg, .cvsignore, html/Kit/dtd/pgip.dtd, html/Kit/dtd/pgml.dtd, html/smallpage.php, html/screenshot.html, html/smallheader.html, html/smallpage.html, html/proofgen.css, html/register, html/register.html, html/screenshot, html/oldnews.html, html/oldrel.html, html/projects.html, html/news, html/news.html, html/notes.txt, html/main, html/main.html, html/mission.html, html/links, html/links.html, html/mailinglist, html/mailinglist.html, html/index.php, html/index.shtml, html/kit, html/kit.html, html/htmlshow.html, html/htmlshow.php, html/gallery.php, html/header.html, html/head.html, html/hits.html, html/fileshow.php, html/footer.html, html/functions.php3, html/gallery, html/features.html, html/feedback.html, html/feedback.php, html/download, html/download.html, html/elispmarkup.php3, html/features, html/develdownload.php, html/doc, html/doc.html, html/develdownload.html, html/cvsweb.conf, html/devel, html/devel.html, html/counter.php3, html/cvsweb.cgi, html/about, html/about.html, html/.cvsignore, html/ProofGeneralPortrait.eps.gz, hol98/example.sml, hol98/hol98.el, hol98/todo, hol98/x-symbol-hol98.el, generic/span.el, generic/texi-docstring-magic.el, hol98/README, generic/span-extent.el, generic/span-overlay.el, generic/proof.el, generic/proof-x-symbol.el, generic/proof-utils.el, generic/proof-syntax.el, generic/proof-system.el, generic/proof-toolbar.el, generic/proof-splash.el, generic/proof-site.el, generic/proof-shell.el, generic/proof-script.el, generic/proof-indent.el, generic/proof-menu.el, generic/proof-depends.el, generic/proof-easy-config.el, generic/proof-config.el, generic/proof-autoloads.el, generic/proof-compat.el, generic/pg-pgip.el, generic/pg-user.el, generic/pg-xml.el, etc/pgkit/xmltest1.xml, etc/pgkit/xmltest2.xml, generic/_pkg.el, generic/README, etc/patches/duplicated-short-messages-fix.txt, etc/patches/fix-attempt-for-eager-cleaning.txt, etc/lego/multiple/C.l, etc/lego/multiple/D.l, etc/lego/multiple/README, etc/lego/multiple/A.l, etc/lego/multiple/B.l, etc/lego/unsaved-goals.l, etc/lego/error-eg.l, etc/lego/lego-site.el, etc/lego/long-line-backslash.l, etc/isar/multiple/README, etc/lego/GoalGoal.l, etc/isar/multiple/A.thy, etc/isar/multiple/B.thy, etc/isar/multiple/C.thy, etc/isar/multiple/D.thy, etc/isar/bad1.thy, etc/isar/bad2.thy, etc/isar/README, etc/isar/XEmacsSyntacticContextProb.thy, etc/demoisa/README, etc/isar/Parsing.thy, etc/demoisa/A.ML, etc/demoisa/B.ML, etc/demoisa/C.ML, etc/demoisa/D.ML, etc/isa/multiple/foobar/foo.ML, etc/isa/thy/test.ML, etc/isa/multiple/D.thy, etc/isa/multiple/Err.ML, etc/isa/multiple/Err.thy, etc/isa/multiple/README, etc/isa/multiple/B.thy, etc/isa/multiple/C.ML, etc/isa/multiple/C.thy, etc/isa/multiple/D.ML, etc/isa/multiple/A.ML, etc/isa/multiple/A.thy, etc/isa/multiple/B.ML, etc/isa/depends/Usedepends.ML, etc/isa/depends/Usedepends.thy, etc/isa/depends/Fib.ML, etc/isa/depends/Fib.thy, etc/isa/depends/Primes.ML, etc/isa/depends/Primes.thy, etc/isa/\backslashname/test.ML, etc/isa/\backslashname/test.thy, etc/isa/long-line-backslash.ML, etc/isa/message-test.ML, etc/isa/settings.ML, etc/isa/xsym.ML, etc/coq/multiple/c.v, etc/isa/goal-matching.ML, etc/coq/multiple/a.v, etc/coq/multiple/b.v, etc/coq/multiple/.cvsignore, etc/coq/multiple/README, etc/coq/unnamed_thm.v, etc/testing-log.txt, etc/proofgeneral-domain.txt, etc/release-log.txt, etc/screenshot-notes.txt, etc/test-schedule.txt, etc/doc-notes.txt, etc/junk.el, etc/profiling.txt, etc/bug-notes.txt, etc/cvs-tips.txt, etc/debugging-tips.txt, etc/announce, etc/README, etc/TESTS, etc/ProofGeneral.menu, etc/ProofGeneral.spec, doc/dir, doc/docstring-magic.el, doc/localdir, doc/README.doc, doc/ProofGeneral.jpg, doc/ProofGeneral.texi, doc/Makefile.doc, doc/PG-adapting.texi, doc/.cvsignore, doc/Makefile, demoisa/demoisa-easy.el, demoisa/demoisa.el, coq/todo, coq/x-symbol-coq.el, demoisa/README, coq/coqtags, coq/example.v, coq/coq.el, coq/BUGS, coq/coq-syntax.el, coq/README, acl2/example.acl2, acl2/x-symbol-acl2.el, bin/proofgeneral, acl2/acl2.el, acl2/README, todo, README.devel, README.windows, REGISTER, TODO, Makefile.xemacs, README, Makefile, Makefile.devel, FAQ, INSTALL, ChangeLog, COPYING, BUGS, CHANGES, AUTHORS:
	Updating branch

	* doc/ProofGeneral.texi:
	Note of what to do

	* generic/proof-script.el: Formatting

	* html/features.html:
	Mention hiding proofs.

	* etc/ProofGeneral.spec:
	Add specific READMEs.

	* etc/cvs-tips.txt:
	Note of secure alt to no password

	* etc/release-log.txt:
	Ready for release

	* etc/announce: Update for 3.3

	* plastic/README, twelf/README, isa/README, isar/README, lego/README, phox/README, hol98/README, coq/README, generic/README, acl2/README:
	Add specific install instrs, rearrange.

	* INSTALL:
	Move specific install instructions into subdirs

	* isa/isa.el:
	Add settings for testing trace buffers.

	* CHANGES:
	Note about tracing buffers for developers

	* generic/proof-shell.el:
	Added handling of tracing buffers using proof-shell-spill-output-regexp.

	* generic/proof-config.el:
	Added proof-shell-spill-output-regexp

2001-09-03  David Aspinall  <da@proofgeneral.org>

	* README.devel: Text

	* ChangeLog: Trim dups

	* README.windows: Add author

	* TODO, CHANGES:
	Updated

	* isa/Example.ML:
	Accidental commit; revert to original.

	* isar/isar.el:
	Set proof-goal-with-hole-regexp

	* generic/proof-config.el:
	Change colour of locked region.

	* generic/proof-shell.el:
	Fix bracket bug.

	* generic/proof-script.el:
	Show/hide all proofs: add redisplay for FSF
	Use new functions pg-set-span-helphighlights and pg-span-name
	to set help echo, balloon help, mouse highlight, and context
	menu.

	* generic/proof-depends.el:
	Use pg-set-span-helphightlights for unhighlighting.

	* generic/pg-user.el:
	Generalise context menu for other spans; grey out show/hide when unavailable.

	* html/main.html: Join paras

	* ChangeLog: Updated.

	* html/features.html: Text

	* html/features.html:
	Fix link to screenshot

	* html/doc.html: Improve layout

	* doc/PG-adapting.texi, doc/ProofGeneral.texi:
	Update version numbers, time stamps.

	* html/download.html:
	Typo.  Update Emacs version to 20.7.

	* ChangeLog: Updated.

	* html/oldrel.php: Update branch

	* html/download.html: PHP file

	* html/oldrel.html, html/oldrel.php:
	Renamed file

	* etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el:
	Set version tag for new release.

	* html/download.html:
	Please try devel version

	* bin/proofgeneral, demoisa/demoisa.el:
	Accidental update; revert to previous

	* demoisa/README: Rearrange

	* twelf/twelf.el, twelf/x-symbol-twelf.el, twelf/twelf-old.el, plastic/todo, twelf/example.elf, twelf/README, twelf/twelf-font.el, plastic/plastic.el, plastic/plastic-syntax.el, plastic/test.lf, phox/phox.el, plastic/README, phox/phox-outline.el, phox/phox-sym-lock.el, phox/phox-tags.el, phox/example.phx, phox/phox-extraction.el, phox/phox-font.el, phox/phox-fun.el, lego/readonly/readonly.l, papers/README, phox/README, lego/legotags, lego/todo, lego/x-symbol-lego.el, lego/example2.l, lego/lego.el, lego/lego-syntax.el, lego/BUGS, lego/example.l, lego/README, isar/todo, isar/isar.el, isar/isar-keywords.el, isar/isar-syntax.el, isar/BUGS, isar/Example.thy, isar/interface, isar/README, isa/todo, isa/x-symbol-isabelle.el, isa/isabelle-system.el, isa/thy-mode.el, isa/isa.el, isa/interface, isa/interface-setup.el, isa/isa-syntax.el, isa/depends.ML, isa/Example2.ML, isa/README, isa/BUGS, isa/Example.ML, isa/Example.thy, isa/Example-Xsym.ML, images/gimp/.cvsignore, images/gimp/scripts/proofgeneral.scm, images/use.8bit.xpm, images/use.xcf, images/use.xpm, images/undo.8bit.xpm, images/undo.xcf, images/undo.xpm, images/retract.xpm, images/state.8bit.xpm, images/state.xcf, images/state.xpm, images/restart.xpm, images/retract.8bit.xpm, images/retract.xcf, images/qed.xpm, images/restart.8bit.xpm, images/restart.xcf, images/pgicon.png, images/pgmini.xpm, images/qed.8bit.xpm, images/qed.xcf, images/pg-text.xcf, images/pg-text.8bit.gif, images/pg-text.gif, images/pg-text.jpg, images/next.xcf, images/next.xpm, images/notes.txt, images/next.8bit.xpm, images/lego-badge.xcf, images/isabelle_transparent.8bit.gif, images/isabelle_transparent.gif, images/isabelle_transparent.xcf, images/isabelle-badge.xcf, images/info.xpm, images/interrupt.8bit.xpm, images/interrupt.xcf, images/interrupt.xpm, images/help.xpm, images/info.8bit.xpm, images/info.xcf, images/goto.xcf, images/goto.xpm, images/help.8bit.xpm, images/help.xcf, images/goto.8bit.xpm, images/goal_large.xcf, images/goal.8bit.xpm, images/goal.xcf, images/goal.xpm, images/find.xpm, images/fireworks.xcf, images/find.8bit.xpm, images/find.xcf, images/context.xpm, images/coq-badge.xcf, images/command.xcf, images/command.xpm, images/context.8bit.xpm, images/context.xcf, images/abort.xpm, images/blank.xcf, images/command.8bit.xpm, images/abort.8bit.xpm, images/abort.xcf, images/README, images/ProofGeneral.jpg, images/ProofGeneral.xcf, images/ProofGeneral.8bit.gif, images/ProofGeneral.gif, images/.cvsignore, images/Makefile, html/projects/test.html, html/projects/thybrowse.html, html/projects/webreplay.html, html/projects/xmlpgip.html, html/projects/pgip.html, html/projects/pgml.html, html/projects/reelcase.html, html/projects/scrgen.html, html/projects/hol.html, html/projects/isapbp.html, html/projects/mm.html, html/projects/outline.html, html/projects/coqfile.html, html/projects/coqpbp.html, html/projects/corba.html, html/projects/acs.html, html/papers/pgtalk.pdf, html/papers/pgoutline.ps.gz, html/papers/pgoutline.pdf, html/images/whole-man.jpg, html/images/whole-man-thumb.jpg, html/images/silverrule.gif, html/images/vh40.gif, html/images/whip.jpg, html/images/whip-thumb.jpg, html/images/pg-text.gif, html/images/portrait.jpg, html/images/portrait-thumb.jpg, html/images/pg-lego-console.png, html/images/pg-lego-screenshot.png, html/images/pg-lego-thumb.png, html/images/pg-isar-thumb.png, html/images/pg-lego-console-thumb.png, html/images/pg-isar-screenshot.png, html/images/pg-isa-screenshot.png, html/images/pg-isa-thumb.png, html/images/pg-coq-thumb.png, html/images/isabelle.gif, html/images/lego-badge.gif, html/images/pg-coq-screenshot.png, html/images/canvaswallpaper.jpg, html/images/coq-badge.gif, html/images/coqlogo4.gif, html/images/coqlogo4.xcf, html/images/isabelle-badge.gif, html/images/bullethole.gif, html/images/PG-small.jpg, html/images/ProofGeneral.jpg, html/images/.cvsignore, html/images/IsaPGscreen.jpg, .cvsignore, html/Kit/dtd/pgip.dtd, html/Kit/dtd/pgml.dtd, html/smallpage.php, html/screenshot.html, html/smallheader.html, html/smallpage.html, html/proofgen.css, html/register, html/register.html, html/screenshot, html/oldnews.html, html/oldrel.html, html/projects.html, html/news, html/news.html, html/notes.txt, html/main, html/main.html, html/mission.html, html/links, html/links.html, html/mailinglist, html/mailinglist.html, html/index.php, html/index.shtml, html/kit, html/kit.html, html/htmlshow.html, html/htmlshow.php, html/gallery.php, html/header.html, html/head.html, html/hits.html, html/fileshow.php, html/footer.html, html/functions.php3, html/gallery, html/features.html, html/feedback.html, html/feedback.php, html/download, html/download.html, html/elispmarkup.php3, html/features, html/develdownload.php, html/doc, html/doc.html, html/develdownload.html, html/cvsweb.conf, html/devel, html/devel.html, html/counter.php3, html/cvsweb.cgi, html/about, html/about.html, html/.cvsignore, html/ProofGeneralPortrait.eps.gz, hol98/example.sml, hol98/hol98.el, hol98/todo, hol98/x-symbol-hol98.el, generic/span.el, generic/texi-docstring-magic.el, hol98/README, generic/span-extent.el, generic/span-overlay.el, generic/proof.el, generic/proof-x-symbol.el, generic/proof-utils.el, generic/proof-syntax.el, generic/proof-system.el, generic/proof-toolbar.el, generic/proof-splash.el, generic/proof-site.el, generic/proof-shell.el, generic/proof-script.el, generic/proof-indent.el, generic/proof-menu.el, generic/proof-depends.el, generic/proof-easy-config.el, generic/proof-config.el, generic/proof-autoloads.el, generic/proof-compat.el, generic/pg-pgip.el, generic/pg-user.el, generic/pg-xml.el, etc/pgkit/xmltest1.xml, etc/pgkit/xmltest2.xml, generic/_pkg.el, generic/README, etc/patches/duplicated-short-messages-fix.txt, etc/patches/fix-attempt-for-eager-cleaning.txt, etc/lego/multiple/C.l, etc/lego/multiple/D.l, etc/lego/multiple/README, etc/lego/multiple/A.l, etc/lego/multiple/B.l, etc/lego/unsaved-goals.l, etc/lego/error-eg.l, etc/lego/lego-site.el, etc/lego/long-line-backslash.l, etc/isar/multiple/README, etc/lego/GoalGoal.l, etc/isar/multiple/A.thy, etc/isar/multiple/B.thy, etc/isar/multiple/C.thy, etc/isar/multiple/D.thy, etc/isar/bad1.thy, etc/isar/bad2.thy, etc/isar/README, etc/isar/XEmacsSyntacticContextProb.thy, etc/demoisa/README, etc/isar/Parsing.thy, etc/demoisa/A.ML, etc/demoisa/B.ML, etc/demoisa/C.ML, etc/demoisa/D.ML, etc/isa/multiple/foobar/foo.ML, etc/isa/thy/test.ML, etc/isa/multiple/D.thy, etc/isa/multiple/Err.ML, etc/isa/multiple/Err.thy, etc/isa/multiple/README, etc/isa/multiple/B.thy, etc/isa/multiple/C.ML, etc/isa/multiple/C.thy, etc/isa/multiple/D.ML, etc/isa/multiple/A.ML, etc/isa/multiple/A.thy, etc/isa/multiple/B.ML, etc/isa/depends/Usedepends.ML, etc/isa/depends/Usedepends.thy, etc/isa/depends/Fib.ML, etc/isa/depends/Fib.thy, etc/isa/depends/Primes.ML, etc/isa/depends/Primes.thy, etc/isa/\backslashname/test.ML, etc/isa/\backslashname/test.thy, etc/isa/long-line-backslash.ML, etc/isa/message-test.ML, etc/isa/settings.ML, etc/isa/xsym.ML, etc/coq/multiple/c.v, etc/isa/goal-matching.ML, etc/coq/multiple/a.v, etc/coq/multiple/b.v, etc/coq/multiple/.cvsignore, etc/coq/multiple/README, etc/coq/unnamed_thm.v, etc/testing-log.txt, etc/proofgeneral-domain.txt, etc/release-log.txt, etc/screenshot-notes.txt, etc/test-schedule.txt, etc/doc-notes.txt, etc/junk.el, etc/profiling.txt, etc/bug-notes.txt, etc/cvs-tips.txt, etc/debugging-tips.txt, etc/announce, etc/README, etc/TESTS, etc/ProofGeneral.menu, etc/ProofGeneral.spec, doc/dir, doc/docstring-magic.el, doc/localdir, doc/README.doc, doc/ProofGeneral.jpg, doc/ProofGeneral.texi, doc/Makefile.doc, doc/PG-adapting.texi, doc/.cvsignore, doc/Makefile, demoisa/demoisa-easy.el, demoisa/demoisa.el, coq/todo, coq/x-symbol-coq.el, demoisa/README, coq/coqtags, coq/example.v, coq/coq.el, coq/BUGS, coq/coq-syntax.el, coq/README, acl2/example.acl2, acl2/x-symbol-acl2.el, bin/proofgeneral, acl2/acl2.el, acl2/README, todo, README.devel, README.windows, REGISTER, TODO, Makefile.xemacs, README, Makefile, Makefile.devel, FAQ, INSTALL, ChangeLog, COPYING, BUGS, CHANGES, AUTHORS:
	Updating branch

	* doc/ProofGeneral.texi:
	Note of what to do

	* generic/proof-script.el: Formatting

	* html/features.html:
	Mention hiding proofs.

	* etc/ProofGeneral.spec:
	Add specific READMEs.

	* etc/cvs-tips.txt:
	Note of secure alt to no password

	* etc/release-log.txt:
	Ready for release

	* etc/announce: Update for 3.3

	* plastic/README, twelf/README, isa/README, isar/README, lego/README, phox/README, hol98/README, coq/README, generic/README, acl2/README:
	Add specific install instrs, rearrange.

	* INSTALL:
	Move specific install instructions into subdirs

	* isa/isa.el:
	Add settings for testing trace buffers.

	* CHANGES:
	Note about tracing buffers for developers

	* generic/proof-shell.el:
	Added handling of tracing buffers using proof-shell-spill-output-regexp.

	* generic/proof-config.el:
	Added proof-shell-spill-output-regexp

2001-09-02  David Aspinall  <da@proofgeneral.org>

	* ChangeLog: Updated.

	* etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el:
	Set version tag for new release.

2001-09-02  David Aspinall  <da@proofgeneral.org>

	* ChangeLog: Updated.

	* etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el:
	Set version tag for new release.

2001-08-31  Markus Wenzel  <wenzelm@informatik.tu-muenchen.de>

	* isa/interface, isar/interface:
	handle relative heap paths gracefully;

	* isar/isar-keywords.el:
	back to *official* Isabelle99-2 (later Isabelle dists will provide
	  their own copy of this file);

2001-08-31  David Aspinall  <da@proofgeneral.org>

	* CHANGES: Improved explanation

	* doc/ProofGeneral.texi:
	Something about dependencies feature

	* CHANGES:
	Added note about dependency feature.

	* generic/proof-depends.el:
	(Almost) complete rewrite

	* generic/proof-autoloads.el: Updated

	* generic/proof-script.el:
	Move theorem dependency code into proof-depends.el.

	Added 'controlspan property to proof body spans: action will be
	controlled from the control span.  (The 'goalsave is the parent).

	Replace 'highlight face with 'proof-mouse-highlight-face throughout.

	* generic/pg-user.el:
	Added copy command, call to dependency menu if proof-depends is loaded.

	* isa/depends.ML:
	Add simulations of more qed commands, also sort and uniquify dependencies.

	* generic/proof-config.el:
	Add new proof-mouse-highlight-face to use instead of default.  Fix dependency faces.

2001-08-31  Markus Wenzel  <wenzelm@informatik.tu-muenchen.de>

	* isar/isar-keywords.el:
	new commands (proof terms, code generator);

2001-08-31  David Aspinall  <da@proofgeneral.org>

	* ChangeLog: Remove duplicate entries

	* generic/proof-config.el:
	Add faces for theorem dependencies.

	* etc/coq/multiple/README: Explanation

	* AUTHORS: Add DvO to list

	* AUTHORS: Add Christophe to list

	* coq/coq.el:
	Add auto-compile-vos experimental setting for automatic multiple files.

	* BUGS: Remove minibuffer bug

	* isa/thy-mode.el:
	Fix for names of functions in proof-depends

	* isa/isa.el:
	Add setting for turning on theorem dependency tracking

	* isa/depends.ML:
	Update for Isabelle99-2

	* generic/proof-depends.el, generic/proof-script.el:
	Clean up of proof-depends

	* generic/proof-menu.el:
	Skip settings which have no PA command in proof-assistant-settings-cmd

	* generic/proof-shell.el:
	Add proof-shell-kill-function-hooks

2001-08-30  Markus Wenzel  <wenzelm@informatik.tu-muenchen.de>

	* isa/interface, isar/interface:
	include ISABELLE_HOME_USER/etc/isar-keywords.el or
	  ISABELLE_HOME/etc/isar-keywords.el if available;

	* isa/README, isar/README, isar/todo:
	updated;

	* generic/proof-script.el:
	pg-add-proof-element: removed accidential (?) dynamic scoping on
	  proofbodyspan;
	handle proof-script-integral-proofs;

	* generic/proof-config.el:
	added proof-script-integral-proofs ("Whether the complete text after a
	  goal confines the actual proof.");

	* isar/isar.el:
	proof-script-integral-proofs t;

2001-08-30  David Aspinall  <da@proofgeneral.org>

	* ChangeLog: Updated.

	* CHANGES: Clarify 6.3.1 for multi file

	* isa/isabelle-system.el:
	Fix interrupt hook for PolyML 4 in recent Isabelle

	* etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el:
	Set version tag for new release.

	* generic/proof-shell.el:
	Add reassurance to interrupt warning to make Markus happier.

	* html/download.html:
	Note about XEmacs 21 and x-symbol

	* isa/isabelle-system.el:
	Set proof-shell-pre-interrupt-hook for PolyML (not just PolyML 3).

	* CHANGES:
	More about invisible proofs and multiple files in Coq.  X-symbol compat

	* generic/proof-x-symbol.el:
	Updates for recent version of X-symbol, which has no file called x-symbol-autoloads.

	* generic/proof-menu.el:
	Add :eval form for defpacustom to define PA-specific PG settings as well as PA settings.

	* generic/proof.el:
	Add variable proof-previous-script-buffer

	* generic/proof-script.el:
	fixes for FSF Emacs for searching for goal span (don't call goal-command-p on empty string).  Fix bug in add-proof-element for disappearing proofs setting.  Add setting of proof-previous-script-buffer when scripting deactivated

	* generic/proof-compat.el:
	Added implementation of remassq for FSF Emacs

	* generic/pg-user.el:
	pg-insert-last-output-as-comment strips special annotations from last output before inserting as comment.

2001-08-30  David Aspinall  <da@proofgeneral.org>

	* CHANGES: Clarify 6.3.1 for multi file

	* isa/isabelle-system.el:
	Fix interrupt hook for PolyML 4 in recent Isabelle

	* etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el:
	Set version tag for new release.

	* generic/proof-shell.el:
	Add reassurance to interrupt warning to make Markus happier.

	* html/download.html:
	Note about XEmacs 21 and x-symbol

	* isa/isabelle-system.el:
	Set proof-shell-pre-interrupt-hook for PolyML (not just PolyML 3).

	* CHANGES:
	More about invisible proofs and multiple files in Coq.  X-symbol compat

	* generic/proof-x-symbol.el:
	Updates for recent version of X-symbol, which has no file called x-symbol-autoloads.

	* generic/proof-menu.el:
	Add :eval form for defpacustom to define PA-specific PG settings as well as PA settings.

	* generic/proof.el:
	Add variable proof-previous-script-buffer

	* generic/proof-script.el:
	fixes for FSF Emacs for searching for goal span (don't call goal-command-p on empty string).  Fix bug in add-proof-element for disappearing proofs setting.  Add setting of proof-previous-script-buffer when scripting deactivated

	* generic/proof-compat.el:
	Added implementation of remassq for FSF Emacs

	* generic/pg-user.el:
	pg-insert-last-output-as-comment strips special annotations from last output before inserting as comment.

2001-08-28  David Aspinall  <da@proofgeneral.org>

	* doc/PG-adapting.texi, doc/ProofGeneral.texi:
	Fix web page for kit

2001-08-28  Pierre Courtieu  <courtieu@lri.fr>

	* doc/ProofGeneral.texi:
	added something in the doc about coq-version-is-V7.

	* coq/coq.el:
	Added something in the doc about coq-version-is-V7, and made the setting of
	this variable more trustable with (concat coq-prog-name "-v").

2001-08-28  David Aspinall  <da@proofgeneral.org>

	* ChangeLog: Updated.

	* etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el:
	Set version tag for new release.

	* generic/proof-script.el:
	Change of proof span type back to goalsave fix

	* lego/lego.el, coq/coq.el, phox/phox-fun.el, isar/isar.el:
	Change of proof span type back to goalsave

	* generic/proof-splash.el:
	Remove dependent setting of timeout, since bin calls different fn now.

	* bin/proofgeneral:
	Call function which always waits to prevent odd mode selection bug.

	* generic/proof-splash.el: Trivial

	* generic/proof-splash.el:
	Remove mention of toolbar variable.  Make timeouts vary according to how started.

	* generic/proof-splash.el:
	Timeout happens as intended now, while loading some parts of PG.

	* html/header.html, html/proofgen.css:
	Improve stylesheet syntax, make menubar smaller

2001-08-17  David Aspinall  <da@proofgeneral.org>

	* ChangeLog: Updated.

	* etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el:
	Set version tag for new release.

	* generic/proof-script.el:
	Trim visibility implementation:
	   - remove visibility specs and script portion records during undo
	   - clear visibility specs on restart

	* generic/span-extent.el, generic/span-overlay.el:
	Add span-delete-action hook

	* CHANGES: Minibuffer contents bug fix

	* generic/proof-utils.el:
	Fix bug in proof-display-and-keep-buffer which had resulted in switching minibuffer windows buffer.

2001-08-16  David Aspinall  <da@proofgeneral.org>

	* ChangeLog: Updated.

	* etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el:
	Set version tag for new release.

	* doc/ProofGeneral.texi:
	Document visibility control

	* html/devel.html:
	Add link to browse files

	* html/download.html:
	Add link to browse package

	* html/develdownload.php:
	Add link to individual files

	* CHANGES:
	Move visibility item up, removed "in progress"

	* generic/proof-shell.el:
	Switch back to using goalsave spans in PBP code

	* generic/proof-config.el, generic/proof-toolbar.el:
	Add hide/show commands instead of make proofs visible

	* generic/proof-script.el:
	Generate intermediate proof span for contents of proof; other becomes 'goalsave again.  Add idiom property.

	* generic/pg-user.el:
	Function name fixes, use idiom property in span for popup menu name.

2001-08-15  David Aspinall  <da@proofgeneral.org>

	* html/gallery.php:
	Fix screenshots link

	* html/gallery: Fix again.

	* html/gallery: Fix link

2001-08-10  David Aspinall  <da@proofgeneral.org>

	* ChangeLog: Updated.

	* CHANGES: Explain symptom properly

	* generic/proof-script.el:
	Use proof-looking-at-syntactic-context function from proof-syntax, as suggested by Markus

	* generic/proof-syntax.el:
	Found another instance of buffer-syntactic-context

	* ChangeLog: Updated.

	* etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el:
	Set version tag for new release.

	* Makefile.devel:
	Put all in dist except pgkit

	* README:
	Rearrange list of assistants, note REGISTER.

	* FAQ: Remove note about 3.1

	* BUGS: Comment about win32 XEmacs

	* generic/proof-compat.el:
	Workaround for buffer-syntactic-context bug in XEmacs 21.1

	* generic/proof-script.el, isar/isar.el:
	Change buffer-syntactic-context -> proof-buffer-syntactic-context

	* etc/isar/XEmacsSyntacticContextProb.thy:
	Bug test case, note workaround date

	* etc/isar/XEmacsSyntacticContextProb.thy:
	Bug test case

	* CHANGES:
	Note of bug fix for buffer-syntactic-context

2001-08-09  Markus Wenzel  <wenzelm@informatik.tu-muenchen.de>

	* isa/x-symbol-isabelle.el:
	fixed potential regexp typo (!?);

2001-08-03  David Aspinall  <da@proofgeneral.org>

	* CHANGES:
	Note about improved win32 support

	* ChangeLog: Updated.

	* etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el:
	Set version tag for new release.

	* html/fileshow.php:
	Fix link back to fileshow.php

	* html/fileshow.html: Renamed file

	* html/main.html: Fix screenshot link

2001-08-01  David Aspinall  <da@proofgeneral.org>

	* doc/ProofGeneral.texi, doc/PG-adapting.texi:
	Update last updated, copyright

	* README.windows: Formatting

	* README: Update for 3.3

	* ChangeLog: Updated.

	* html/screenshot.html, html/about.html, html/oldnews.html:
	Fix links to gallery

	* html/gallery.html: Deleted files.

	* html/gallery: Renamed file

	* html/gallery.html: Moved to .php

	* html/about.html: Fix typo

	* html/gallery.php, html/gallery.html:
	Renamed file

	* html/news.html: Added news

	* ChangeLog: Updated.

	* etc/ProofGeneral.spec, html/devel.html, generic/proof-site.el, html/develdownload.php:
	Set version tag for new release.

	* generic/proof-autoloads.el:
	Regenerate to remove Christophes patch

	* generic/proof-compat.el, generic/proof-site.el:
	Moved compat hack to proof-site

	* generic/proof-toolbar.el:
	Revert to removing and re-adding specifiers for toolbar,
	so that enablers work at least as well as they did before...

	* generic/proof-compat.el:
	Add a dummy version of package-provide for FSFEmacs.

2001-07-25  Christophe Raffalli  <Christophe.Raffalli@univ-savoie.fr>

	* generic/proof-autoloads.el, generic/proof-splash.el, README.windows:
	*** empty log message ***

	* phox/phox.el, phox/phox-sym-lock.el, phox/phox-fun.el, generic/proof-splash.el, generic/proof-toolbar.el:
	Various changes for win32 compatibility

2001-07-23  David Aspinall  <da@proofgeneral.org>

	* ChangeLog: Updated.

	* etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el:
	Set version tag for new release.

	* generic/proof-menu.el:
	Prevent error msg in proof-display-some-buffers if response dead.

	* generic/proof-shell.el:
	Bug report from Robert Schneck.  Make proof-shell-restart start shell.  Goals display convention, not hack.

2001-07-09  David Aspinall  <da@proofgeneral.org>

	* ChangeLog: Updated.

	* todo:
	TODO for proof-ass fixing added.

	* etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el:
	Set version tag for new release.

	* generic/proof-toolbar.el:
	Clean for compile

	* generic/proof-menu.el:
	Clean for compile: new autload

	* generic/proof-autoloads.el: Refresh

	* generic/pg-xml.el, generic/pg-user.el:
	Clean-up compile

	* generic/proof-compat.el:
	Add require for arch flags, cleaner compilation.

	* generic/pg-pgip.el:
	Fix some bugs shown by byte comp

	* generic/proof-autoloads.el:
	Updated autoloads

	* generic/_pkg.el:
	Package file (old attempt -- not working)

2001-06-22  Christophe Raffalli  <Christophe.Raffalli@univ-savoie.fr>

	* phox/phox.el:
	*** empty log message ***

2001-05-29  David Aspinall  <da@proofgeneral.org>

	* html/main.html: Fix Coq link.

	* ChangeLog: Updated.

	* etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el:
	Set version tag for new release.

	* isa/Example.ML: Remove extra proof."

	* generic/proof-splash.el:
	Display screen only if called interactively

	* doc/ProofGeneral.texi:
	AF2 -> PhoX name change

	* etc/ProofGeneral.spec:
	Add REGISTER to doc files.

	* COPYING: Date 2001

	* html/features.html:
	Fix layout and typo.

	* html/mailinglist.html:
	Include PHP file

	* REGISTER:
	Note about mailing list and registration.

	* html/mailinglist, html/mailinglist.php:
	Renamed file

	* html/mailinglist.html, html/mailinglist.php:
	PHP version.  Also dont mention junk filters.

2001-05-18  Markus Wenzel  <wenzelm@informatik.tu-muenchen.de>

	* isar/isar-keywords.el:
	preliminary addition of "corollary";

2001-05-16  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: Minor

	* bin/proofgeneral:
	Run the display splash command

	* generic/proof-config.el:
	Moved splash settings and basic custom groups elsewhere

	* CHANGES: splash changes.

	* generic/proof-site.el:
	Move loading of compatibility flag, autoloads, basic customization groups here.

	* generic/proof.el:
	Move autoloads loads to proof-site, invoke (proof-splash-message)

	* generic/proof-compat.el:
	Move emacs version compatibility flags to proof-site.el

	* generic/proof-splash.el:
	Move configuration from proof-config here.  Make proof-splash-message display logo or print message.

	* etc/README:
	Doc of spec and menu, patch now removed

2001-05-08  David Aspinall  <da@proofgeneral.org>

	* ChangeLog: Updated.

	* etc/ProofGeneral.menu:
	Fix case to match Mandrake menu.

	* ChangeLog: Updated.

	* etc/ProofGeneral.menu: Fix quotes.

	* html/functions.php3:
	Repair link via htmlshow.php

	* doc/PG-adapting.texi:
	Change info dir entry to appear next to Proof General entry.

	* ChangeLog: Updated.

	* html/develdownload.php:
	Set version tag for new release.

	* Makefile.devel:
	Change DEVELDOWNLOAD to edit correct file

	* ChangeLog: Updated.

	* etc/ProofGeneral.spec:
	Add a line to clear out build root.

	* ChangeLog: Updated.

	* Makefile.devel:
	Forgot to make BUILD dir.

	* ChangeLog: Updated.

	* Makefile.devel:
	Fix cut and past tab error

	* Makefile.devel:
	rpm target: Clean out rpmtopdir, and make subdirs again.  Get full path to tar file

	* ChangeLog: Updated.

	* Makefile.devel:
	Clean out NAME, force link.

	* ChangeLog: Updated.

	* Makefile.devel:
	Include a few files from etc in the distribution, esp .spec file

	* etc/ProofGeneral.menu:
	*** empty log message ***

	* etc/ProofGeneral.patch:
	Deleted files.

	* ChangeLog: Updated.

	* doc/ProofGeneral.texi:
	Fix section title for makeinfo

	* etc/ProofGeneral.spec, html/devel.html, generic/proof-site.el:
	Set version tag for new release.

	* Makefile.devel:
	Dont make SRPM any more.  Use rpm -tb to build binary package from tarball

	* CHANGES: Updates

	* etc/ProofGeneral.spec:
	Updates, removal of patch so that rpm -ta works

	* doc/ProofGeneral.texi:
	Updates for 3.3

	* generic/proof-utils.el:
	Fixes for fontification in Xemacs 21.4

	* generic/proof-site.el, generic/proof-syntax.el, generic/proof-shell.el, generic/proof-easy-config.el, generic/proof-indent.el, generic/proof-menu.el, generic/proof-config.el, generic/pg-pgip.el, generic/pg-user.el, generic/pg-xml.el, generic/proof-compat.el:
	Copyright date updated

	* generic/README:
	Add Markus to list of authors

	* html/main.html:
	preliminary -> experimental

	* html/develdownload.php:
	No longer distrib SRPM

	* html/news.html: New news item

2001-05-03  David Aspinall  <da@proofgeneral.org>

	* generic/proof-splash.el:
	change for Emacs compatibility and FSF/Xemacs update.  Copyright update.

	* generic/proof-script.el:
	Emacs fix  (extent->span).  Copyright update.

2001-05-01  David Aspinall  <da@proofgeneral.org>

	* ChangeLog: Updated.

	* doc/ProofGeneral.texi, doc/Makefile.doc, doc/PG-adapting.texi:
	Try to disable image for now

	* etc/ProofGeneral.spec, html/devel.html, generic/proof-site.el:
	Set version tag for new release.

	* html/devel.html: Change link to kit

	* html/download.html:
	Change link to register page

	* html/feedback.html, html/index.shtml:
	Include php file

	* html/register, html/kit:
	Register and kit shortcuts

	* html/develdownload.html:
	Include php file

	* html/functions.php3:
	Link to php files instead of html

	* html/links, html/main, html/news, html/about, html/devel, html/doc, html/download, html/features:
	Include php instead of html

	* html/smallpage.php, html/htmlshow.php, html/index.php, html/develdownload.php, html/feedback.php, html/fileshow.php:
	Rename some html files php

	* html/index.html: Deleted files.

2001-04-10  Pierre Courtieu  <courtieu@lri.fr>

	* coq/coq.el:
	Modification of proof-script-command-end-regexp to allow commands
	ended by ".eof"

2001-03-20  David Aspinall  <da@proofgeneral.org>

	* ChangeLog: Updated.

	* html/main.html: Fixes to main page

	* html/footer.html:
	Change to my canonical www.dcs web address

	* html/main.html:
	Remove proofgeneral.org on main page

	* ChangeLog: Updated.

	* etc/ProofGeneral.spec, html/devel.html, generic/proof-site.el, html/develdownload.html:
	Set version tag for new release.

	* BUGS:
	strange buffer selection bug reported by Markus

	* doc/PG-adapting.texi: Updated magic

2001-03-20  Pierre Courtieu  <courtieu@lri.fr>

	* coq/coq.el:
	Added the config var proof-script-command-end-regexp fot coq V7.

2001-03-20  David Aspinall  <da@proofgeneral.org>

	* doc/Makefile.doc:
	Use PS fonts in PS file

	* generic/proof-shell.el:
	Remove temporary comments

	* generic/proof-config.el:
	Fix docstring

	* html/feedback.html, html/footer.html, html/functions.php3:
	Changes to use proofgen@dcs for now instead of broken proofgeneral.org

	* html/main.html: Fix to Coq web page

2001-03-19  Christophe Raffalli  <Christophe.Raffalli@univ-savoie.fr>

	* phox/phox-font.el:
	*** empty log message ***

2001-02-26  Pierre Courtieu  <courtieu@lri.fr>

	* coq/coq.el:
	minor change in coq.el to allow to force version of coq, with variable
	coq-version-is-V7

2001-02-20  Christophe Raffalli  <Christophe.Raffalli@univ-savoie.fr>

	* phox/phox.el, phox/example.phx, phox/phox-extraction.el, phox/phox-fun.el, phox/phox-tags.el, html/develdownload.html, html/devel.html, phox/README, generic/proof-site.el, etc/ProofGeneral.spec:
	*** empty log message ***

2001-02-08  Christophe Raffalli  <Christophe.Raffalli@univ-savoie.fr>

	* phox/phox-font.el:
	*** empty log message ***

2001-02-07  David Aspinall  <da@proofgeneral.org>

	* ChangeLog: Updated.

	* etc/ProofGeneral.spec, html/devel.html, html/develdownload.html, generic/proof-site.el:
	Set version tag for new release.

2001-02-07  Christophe Raffalli  <Christophe.Raffalli@univ-savoie.fr>

	* phox/phox.el, phox/phox-font.el, phox/phox-fun.el, phox/phox-tags.el, phox/phox-extraction.el:
	*** empty log message ***

2001-02-06  David Aspinall  <da@proofgeneral.org>

	* etc/ProofGeneral.spec, html/develdownload.html, html/devel.html, generic/proof-site.el:
	Set version tag for new release.

2001-02-02  Christophe Raffalli  <Christophe.Raffalli@univ-savoie.fr>

	* phox/phox-font.el:
	*** empty log message ***

2001-02-01  Markus Wenzel  <wenzelm@informatik.tu-muenchen.de>

	* doc/ProofGeneral.texi:
	updated thms_containing;

2001-02-01  Christophe Raffalli  <Christophe.Raffalli@univ-savoie.fr>

	* phox/phox-sym-lock.el, phox/phox.el, phox/phox-font.el:
	*** empty log message ***

2001-01-24  Markus Wenzel  <wenzelm@informatik.tu-muenchen.de>

	* isa/x-symbol-isabelle.el:
	renamed \<ll> to \<lless> and \<gg> to \<ggreater>;

2001-01-18  Markus Wenzel  <wenzelm@informatik.tu-muenchen.de>

	* isar/isar.el:
	proof-xsym-deactivate-command: use Library.gen_rems (op =) to avoid \\\\;

2001-01-18  Christophe Raffalli  <Christophe.Raffalli@univ-savoie.fr>

	* phox/phox-extraction.el, phox/phox.el, phox/phox-fun.el, phox/phox-tags.el:
	*** empty log message ***

2001-01-12  Markus Wenzel  <wenzelm@informatik.tu-muenchen.de>

	* isa/isa.el: proof-string-match;

2001-01-12  David Aspinall  <da@proofgeneral.org>

	* ChangeLog: Updated.

	* isa/isa.el:
	Fix loading thy mode fist problem: require proof-script since context
	menus are now added for response/goals buffer, which requires proof mode.

2001-01-12  Markus Wenzel  <wenzelm@informatik.tu-muenchen.de>

	* isa/isabelle-system.el, isar/isar.el, isar/isar-syntax.el:
	proof-string-match;

2001-01-12  Markus Wenzel  <wenzelm@informatik.tu-muenchen.de>

	* isa/isabelle-system.el, isar/isar.el, isar/isar-syntax.el:
	proof-string-match;

2001-01-11  Christophe Raffalli  <Christophe.Raffalli@univ-savoie.fr>

	* phox/phox.el:
	*** empty log message ***

2001-01-11  Markus Wenzel  <wenzelm@informatik.tu-muenchen.de>

	* generic/proof-shell.el, generic/pg-xml.el, generic/proof-script.el:
	fixed format strings in message, error, etc.

2001-01-10  Markus Wenzel  <wenzelm@informatik.tu-muenchen.de>

	* isar/isar-syntax.el:
	proper font-lock of isar-keywords-proof-heading;

	* isa/x-symbol-isabelle.el:
	added \<wrong>;

2001-01-09  Markus Wenzel  <wenzelm@informatik.tu-muenchen.de>

	* isa/x-symbol-isabelle.el:
	added \<cedilla>, \<dieresis>, \<acute>, \<hungarumlaut>;

2001-01-05  David Aspinall  <da@proofgeneral.org>

	* ChangeLog: Updated.

	* etc/ProofGeneral.spec, generic/proof-site.el, html/develdownload.html, html/devel.html:
	Set version tag for new release.

2001-01-03  Markus Wenzel  <wenzelm@informatik.tu-muenchen.de>

	* isar/isar-keywords.el:
	added "recdef_tc";