++The forefather of Proof General was LEGO mode, begun in 1994 at the LFCS by Thomas Kleymann. LEGO +mode was an Emacs-based front end for LEGO similar to David Aspinall's +Isamode, +developed at the LFCS since 1992. After 1994, implementations of +proof-by-pointing and script management were added to LEGO mode, and +the code was made generic. The generic basis was developed by +Thomas Kleymann, Dilip Sequeira, Healfdene Goguen and David Aspinall. +The current authors and maintainers of the various instantiations of +Proof General are mentioned on the +
++The Proof General project was coordinated until October 1998 by +Thomas Kleymann, and since then by David Aspinall. The project has +benefited from funding by + +EPSRC, + + +the EC, +and the LFCS. +
+ +
+David Aspinall designed the web pages and graphics for Proof General.
+
+Check the gallery for more publicity
+pictures!
+
+For more on the history of the development of +the Proof General program, see the + +
+ + +
+Have you any questions, comments, or suggestions about Proof General?
+
+Send us a message using this form.
+
+Discuss Proof General with other users and receive +announcements by joining our mailing +list. +
+ + + diff --git a/html/about.phtml b/html/about.phtml deleted file mode 100644 index 7641676d..00000000 --- a/html/about.phtml +++ /dev/null @@ -1,56 +0,0 @@ --The forefather of Proof General was LEGO mode, begun in 1994 at the LFCS by Thomas Kleymann. LEGO -mode was an Emacs-based front end for LEGO similar to David Aspinall's -Isamode, -developed at the LFCS since 1992. After 1994, implementations of -proof-by-pointing and script management were added to LEGO mode, and -the code was made generic. The generic basis was developed by -Thomas Kleymann, Dilip Sequeira, Healfdene Goguen and David Aspinall. -The current authors and maintainers of the various instantiations of -Proof General are mentioned on the -
--The Proof General project was coordinated until October 1998 by -Thomas Kleymann, and since then by David Aspinall. The project has -benefited from funding by - -EPSRC, - - -the EC, -and the LFCS. -
- -
-David Aspinall designed the web pages and graphics for Proof General.
-
-Check the gallery for more publicity
-pictures!
-
-For more on the history of the development of -the Proof General program, see the - -
- - -
-Have you any questions, comments, or suggestions about Proof General?
-
-Send us a message using this form.
-
-Discuss Proof General with other users and receive -announcements by joining our mailing -list. -
- - - diff --git a/html/devel.html b/html/devel.html new file mode 100644 index 00000000..aa418f08 --- /dev/null +++ b/html/devel.html @@ -0,0 +1,111 @@ +
+Proof General follows an open development method.
+
+We welcome code contributions, suggestions, and bug reports, from all
+users and hackers!
+
+We have a mailing list for developers, at
+
+proofgeneral-devel@dcs.ed.ac.uk.
+
+To subscribe (or unsubscribe), send a message to
+
+ majordomo@dcs.ed.ac.uk
+
+with the words "subscribe proofgeneral-devel"
+(or "unsubscribe proofgeneral-devel") in the message body.
+
-Proof General follows an open development method.
-
-We welcome code contributions, suggestions, and bug reports, from all
-users and hackers!
-
-We have a mailing list for developers, at
-
-proofgeneral-devel@dcs.ed.ac.uk.
-
-To subscribe (or unsubscribe), send a message to
-
- majordomo@dcs.ed.ac.uk
-
-with the words "subscribe proofgeneral-devel"
-(or "unsubscribe proofgeneral-devel") in the message body.
-
+Below is the latest pre-release of Proof General, +made available for those who wish to test the latest features or bug +fixes. For developers, this release is also available as a +complete CVS snapshot (further below). +
++Pre-releases of Proof General may be buggy as we add new features and +experiment with them. Nonetheless, we welcome bug reports. But +please make sure you are using the latest pre-release before +reporting problems. +
++Please register if you haven't done so already. +
+ + + ++The manual included with the pre-release may be +updated from that of the +. +
++You can see the current documentation: the user manual in +, + +or +, +and the new separate "adapting" manual, in +, + +or +. +
+ + + ++This version has been tested with XEmacs version 21.1.12 and +(minimally) with FSF Emacs 20.7.1. +We recommend the use of XEmacs; use under FSF Emacs +can no longer be supported. +
++Check the + + file + +for a summary of changes since the last stable version, and +notes about work-in-progress. +
+| gzip'ed tar file | + ++ |
| zip file | ++ |
| RPM package | ++ |
| SRPM package | ++ |
+For install instructions, see +the . +
+ ++
++
+ + + ++This archive is a snapshot from our CVS repository. +
++What's the difference from the user's pre-release above? +The complete archive also includes: +
++You probably don't need to download this if you're only +interested in hacking the Emacs lisp part of the program for a prover +that is currently supported. Note that there are no pre-built +documentation files in the developer's release. +
+ + diff --git a/html/develdownload.phtml b/html/develdownload.phtml deleted file mode 100644 index 499a0b15..00000000 --- a/html/develdownload.phtml +++ /dev/null @@ -1,134 +0,0 @@ - - --Below is the latest pre-release of Proof General, -made available for those who wish to test the latest features or bug -fixes. For developers, this release is also available as a -complete CVS snapshot (further below). -
--Pre-releases of Proof General may be buggy as we add new features and -experiment with them. Nonetheless, we welcome bug reports. But -please make sure you are using the latest pre-release before -reporting problems. -
--Please register if you haven't done so already. -
- - - --The manual included with the pre-release may be -updated from that of the -. -
--You can see the current documentation: the user manual in -, - -or -, -and the new separate "adapting" manual, in -, - -or -. -
- - - --Check the - - file - -for a summary of changes since the last stable version, and -notes about work-in-progress. -
-| gzip'ed tar file | - -- |
| zip file | -- |
| RPM package | -- |
| SRPM package | -- |
-For install instructions, see -the . -
- --
--
- - - --This archive is a snapshot from our CVS repository. -
--What's the difference from the user's pre-release above? -The complete archive also includes: -
--You probably don't need to download this if you're only -interested in hacking the Emacs lisp part of the program for a prover -that is currently supported. Note that there are no pre-built -documentation files in the developer's release. -
- - diff --git a/html/doc.html b/html/doc.html new file mode 100644 index 00000000..e8ae6b98 --- /dev/null +++ b/html/doc.html @@ -0,0 +1,88 @@ +
+Here is the
+ in HTML form, as included in the distribution.
+
+For printing you can download the
+
+(recommended) or the
+.
+
+The manual (in HTML and Info formats), as well as other documentation, +is included in the When +running Proof General the manual is available from the "Proof General" +menu. It should also appear in the system Info pages. +
+ + ++You can discuss Proof General with other users and receive +announcements by joining our mailing +list. +
+ +Ideas for the future of Proof General are given here: +
+A technology overview of Proof General is given here: +
+Proof General supports Script Management as documented in: +
++ It has support for Proof by Pointing, as documented in: +
+
-Here is the
- in HTML form, as included in the distribution.
-
-For printing you can download the
-
-(recommended) or the
-.
-
-The manual (in HTML and Info formats), as well as other documentation, -is included in the When -running Proof General the manual is available from the "Proof General" -menu. It should also appear in the system Info pages. -
- - --You can discuss Proof General with other users and receive -announcements by joining our mailing -list. -
- -Ideas for the future of Proof General are given here: -
-A technology overview of Proof General is given here: -
-Proof General supports Script Management as documented in: -
-- It has support for Proof by Pointing, as documented in: -
--Before downloading Proof General, please -register. -It's free, it only takes a moment. -If you have already registered you do not need to do so again. -
--The statistics collected from registrations will be used to help a -case for support for Proof General, and nothing else. It is likely -that development of Proof General will finish very soon unless -we can find new resources. As a courtesy, we do not make registration -compulsory and I can tell from the server logs that the majority of -people downloading do not register. But if you don't register -now, please consider returning to register later if you find Proof -General interesting or useful. If you don't want to fill the form, -please send an email -directly. -
- --You may like to join the -Proof General -mailing list. -Developers and beta-testers may like to download -a development release -of Proof General. -If you use an old version of a proof assistant, -you may need to download one of the -previous releases. -
--Please check the - -for using Proof General. -
- --To run Proof General, you must have: -
-- -There are also some optional components for using -Proof General: -
-All components mentioned above are distributed under the GPL license. -
--Proof General is available as an archive and an RPM package. -
-
-Both the tarball and the RPM package include the generic elisp
-code,
-code for LEGO, Coq, and Isabelle, installation instructions
-and documentation (in Info and HTML formats).
-
-Documentation is available in other formats -here . -If you want to format the documentation yourself, -you may like to download the -. -
- --This version of Proof General has been tested -with XEmacs 21.1 and FSF Emacs 20.4. -It supports Coq version 6.3, LEGO version 1.3.1 and -Isabelle99. -
--Check the file -for a summary of changes since version 3.0. -
--Check the latest file -(also - - - -) - -before reporting problems. If you find a problem not already mentioned, -please -. -
--To use Proof General, simply unpack the sources with -
-- tar xpzf ProofGeneral-3.1.tar.gz --
-(use gunzip first in place of z if you don't have
-GNU tar),
and then add this one line to your .emacs file:
-
- (load-file "directory/generic/proof-site.el") --
-Where directory is the directory in which you unpacked
-the sources.
-
-If you use the RPM package, directory is
-/usr/share/emacs/ProofGeneral
-
-If you're using Windows, then download the zip file.
-
-Use a zip file utility to unpack it somewhere, for example
-c:\\ProofGeneral
-
-Further customization is possible via the Customize menus in
-Emacs.
-
-See the
-file in the distribution for more details.
-
-Contrary to what you may expect from the documentation of -X-Symbol, it's very easy to install and configures itself -automatically. -
--Simply download the binary package file, and do something -like this to install in your home directory: -
-- mkdir -p ~/.xemacsdiff --git a/html/features.html b/html/features.html new file mode 100644 index 00000000..372ab17b --- /dev/null +++ b/html/features.html @@ -0,0 +1,182 @@ +
- cd ~/.xemacs
- tar xpzf ../x-symbol-pkg.tar.gz
-
+It doesn't matter if you're an Emacs militant or a pacifist! +
+ +
+Proof General is designed to be useful for novices and expert users alike.
+
+It will be useful to you if you use a proof assistant, and
+you'd like an interface with the following features...
+
+ Proof General colours a proof script to show the state in the proof + assistant. Parts of a proof script that have been processed are + displayed in blue and are "locked" -- they cannot be edited. Parts + of the script currently being processed by the proof assistant are + shown in red. Proof General has commands for processing new parts + of the buffer, or undoing already processed parts. +
++ Take a look at these + screenshots + of Proof General to see script managament in action. +
++ Despite this more friendly communication model, Proof General does not + commandeer the proof assistant shell: the user still has complete + access to it if necessary. +
++ Dependencies between script files are either communicated from the + proof assistant to Proof General, or maintained automatically by + Proof General (based on the order in which files were processed). +
++ Proof by pointing uses the interface to highlight subterms under the + mouse, and sends messages asking the prover for hints to proceed. + Proof General also uses the subterm structure to make it easy to cut + and paste from complicated terms. +
+ ++ Using the toolbar, you can replay proofs without knowing any + low-level commands of the proof assistant or any Emacs hot-keys! +
+ Additionally, the toolbar commands and many more besides are + available on menus; you don't need to know magical key presses for + any features. +
+ ++ Proof General decorates proof scripts: proof commands are + highlighted and different fonts may be used for definitions and + assumptions, for example. +
++ +
+
+ Most importantly, Proof General is generic, so you can adapt it to + a new proof assistant with surprisingly little effort. +
+ Adapting for a new proof assistant is mainly a matter of setting + some variables with regular expressions to help parse output from + the prover, and setting other variables with commands to send to the + prover. See this basic + . + To get the most from Proof General (proof by pointing, for + example), it may be necessary to put some hooks in + the output routines of the proof assistant. +
+ Please feel free to download Proof General to customize it for a new + system, and + + how you get on. ++For (even) more details of the above features, see the + +
+ diff --git a/html/features.phtml b/html/features.phtml deleted file mode 100644 index 372ab17b..00000000 --- a/html/features.phtml +++ /dev/null @@ -1,182 +0,0 @@ --It doesn't matter if you're an Emacs militant or a pacifist! -
- -
-Proof General is designed to be useful for novices and expert users alike.
-
-It will be useful to you if you use a proof assistant, and
-you'd like an interface with the following features...
-
- Proof General colours a proof script to show the state in the proof - assistant. Parts of a proof script that have been processed are - displayed in blue and are "locked" -- they cannot be edited. Parts - of the script currently being processed by the proof assistant are - shown in red. Proof General has commands for processing new parts - of the buffer, or undoing already processed parts. -
-- Take a look at these - screenshots - of Proof General to see script managament in action. -
-- Despite this more friendly communication model, Proof General does not - commandeer the proof assistant shell: the user still has complete - access to it if necessary. -
-- Dependencies between script files are either communicated from the - proof assistant to Proof General, or maintained automatically by - Proof General (based on the order in which files were processed). -
-- Proof by pointing uses the interface to highlight subterms under the - mouse, and sends messages asking the prover for hints to proceed. - Proof General also uses the subterm structure to make it easy to cut - and paste from complicated terms. -
- -- Using the toolbar, you can replay proofs without knowing any - low-level commands of the proof assistant or any Emacs hot-keys! -
- Additionally, the toolbar commands and many more besides are - available on menus; you don't need to know magical key presses for - any features. -
- -- Proof General decorates proof scripts: proof commands are - highlighted and different fonts may be used for definitions and - assumptions, for example. -
-- -
-
- Most importantly, Proof General is generic, so you can adapt it to - a new proof assistant with surprisingly little effort. -
- Adapting for a new proof assistant is mainly a matter of setting - some variables with regular expressions to help parse output from - the prover, and setting other variables with commands to send to the - prover. See this basic - . - To get the most from Proof General (proof by pointing, for - example), it may be necessary to put some hooks in - the output routines of the proof assistant. -
- Please feel free to download Proof General to customize it for a new - system, and - - how you get on. --For (even) more details of the above features, see the - -
- diff --git a/html/feedback.html b/html/feedback.html new file mode 100644 index 00000000..17dc974c --- /dev/null +++ b/html/feedback.html @@ -0,0 +1,89 @@ + + +
+Please use the form below to send us comments, suggestions,
+or offers to help with Proof Generl development.
+
+Or send email directly to
+the
+Proof General maintainer
+<feedback@proofgeneral.org>.
+
+You can also report a bug using this form, although it would +be more helpful to do this from within Emacs, using the +"Proof General -> Submit bug report" menu command. +
+ + + +Dear " . $from . ",\n"; }; + print ""; + print "Thank-you for sending us feedback"; + if ($subject != "") { print " about " . $subject; }; + print ".
\n"; + print "If you provided a valid return email address, somebody from the Proof General team will acknowledge your message after it has been read."; + print "
"; + + mail("feedback@proofgeneral.org", + "[Web Feedback Form]: " . $subject, + $message, + "Reply-To: " . $from . "\n"); + + click_to_go_back(); + + footer(); +endif; +?> diff --git a/html/feedback.phtml b/html/feedback.phtml deleted file mode 100644 index 17dc974c..00000000 --- a/html/feedback.phtml +++ /dev/null @@ -1,89 +0,0 @@ - - -
-Please use the form below to send us comments, suggestions,
-or offers to help with Proof Generl development.
-
-Or send email directly to
-the
-Proof General maintainer
-<feedback@proofgeneral.org>.
-
-You can also report a bug using this form, although it would -be more helpful to do this from within Emacs, using the -"Proof General -> Submit bug report" menu command. -
- - - -Dear " . $from . ",\n"; }; - print ""; - print "Thank-you for sending us feedback"; - if ($subject != "") { print " about " . $subject; }; - print ".
\n"; - print "If you provided a valid return email address, somebody from the Proof General team will acknowledge your message after it has been read."; - print "
"; - - mail("feedback@proofgeneral.org", - "[Web Feedback Form]: " . $subject, - $message, - "Reply-To: " . $from . "\n"); - - click_to_go_back(); - - footer(); -endif; -?> diff --git a/html/fileshow.html b/html/fileshow.html new file mode 100644 index 00000000..a13857e7 --- /dev/null +++ b/html/fileshow.html @@ -0,0 +1,24 @@ +\n"; + /* I hope this is enough to prevent access outside cwd */ + if (substr($filename,0,1)=="." or + substr($filename,0,1)=="/" or + substr($filename,0,1)=="~") { + print "Sorry, can't show you that file!\n"; + } elseif (substr($filename,-3)==".el") { + elisp_markup($filename,"fileshow.phtml"); + } else { + outline_markup($filename,"fileshow.phtml",$expanded); + } + print "\n"; + print "
+
+
+Web pages by
+David Aspinall.
+
-
-
-Web pages by
-David Aspinall.
-++ + ++Here are some publicity pictures for Proof General. They were created +by David Aspinall in his spare time, using the excellent freeware +programs GIMP and Blender. The General himself is +based on a commercial mesh given away by +Viewpoint. +
++Click on a thumbnail to see a full-size images. All full-size images +are 720x990 pixel JPGs (a nice size to print at 180dpi on A5 paper). +Please download and print for your own use! +
+Copyright for the images is held by +David Aspinall. +Please do not publish the images or incorporate them into other +work without his permission. If you have comments or suggestions, +or if you would like a copy of one of the images +in another size or format, +please contact us. +
+ + ++For pictures of what Proof General looks like in use, +see the screenshots page. +
+
+
+
+
+ |
+
+
+Proof General portrait |
+
+
+
+ |
+
+
+New Recruits Wanted |
+
+
+
+ |
+
+
+Scary boots! |
-- - --Here are some publicity pictures for Proof General. They were created -by David Aspinall in his spare time, using the excellent freeware -programs GIMP and Blender. The General himself is -based on a commercial mesh given away by -Viewpoint. -
--Click on a thumbnail to see a full-size images. All full-size images -are 720x990 pixel JPGs (a nice size to print at 180dpi on A5 paper). -Please download and print for your own use! -
-Copyright for the images is held by -David Aspinall. -Please do not publish the images or incorporate them into other -work without his permission. If you have comments or suggestions, -or if you would like a copy of one of the images -in another size or format, -please contact us. -
- - --For pictures of what Proof General looks like in use, -see the screenshots page. -
-
|
-
-
-
- |
-
-
-Proof General portrait |
|
-
-
-
- |
-
-
-New Recruits Wanted |
|
-
-
-
- |
-
-
-Scary boots! |
+
+
+
+ |
+
+ 
+ Organize your proofs!+ ';
+ $WANTED=$HTTP_GET_VARS["page"];
+ print " |
|
-
-
-
- |
-
-
- Organize your proofs!-';
- $WANTED=$HTTP_GET_VARS["page"];
- print " |
+Here are some links to related things. +If you have any suggestions +for links to include here, please +. +
+ +-Here are some links to related things. -If you have any suggestions -for links to include here, please -. -
- -+The mailing list address is + +users@proofgeneral.org. + +
+ +
+To subscribe or unsubscribe, you can fill in the form below.
+
+Or send a message to
+
+ majordomo@proofgeneral.org
+
+with the words "subscribe proofgeneral"
+(or "unsubscribe proofgeneral") in the message body.
+
+Since its beginning, the mailing list has been a low-volume list (one +message every few months). If the volume increases significantly due +to user interaction, we will introduce a separate mailing list for +announcements. Junk mail filters are applied to the list to +prevent junk being forwarded to list members. +
+ ++
+Dear " . $from . ",\n"; }; + print "";
+ print "Your request to " . $request . " the proof general mailing list has been submitted.
";
+ print "Thank-you!";
+ print "
"; + + click_to_go_back(); + + footer(); + endif; +?> + diff --git a/html/mailinglist.phtml b/html/mailinglist.phtml deleted file mode 100644 index b6336f45..00000000 --- a/html/mailinglist.phtml +++ /dev/null @@ -1,100 +0,0 @@ - -
-The mailing list address is - -users@proofgeneral.org. - -
- -
-To subscribe or unsubscribe, you can fill in the form below.
-
-Or send a message to
-
- majordomo@proofgeneral.org
-
-with the words "subscribe proofgeneral"
-(or "unsubscribe proofgeneral") in the message body.
-
-Since its beginning, the mailing list has been a low-volume list (one -message every few months). If the volume increases significantly due -to user interaction, we will introduce a separate mailing list for -announcements. Junk mail filters are applied to the list to -prevent junk being forwarded to list members. -
- --
-Dear " . $from . ",\n"; }; - print "";
- print "Your request to " . $request . " the proof general mailing list has been submitted.
";
- print "Thank-you!";
- print "
"; - - click_to_go_back(); - - footer(); - endif; -?> - diff --git a/html/main.html b/html/main.html new file mode 100644 index 00000000..7844d527 --- /dev/null +++ b/html/main.html @@ -0,0 +1,138 @@ +
+Proof General is a generic interface for proof assistants, +currently based on Emacs. +It has been developed at the +LFCS +in the University of Edinburgh. +
++Proof General +works best under +XEmacs, but can also be used with +FSF GNU Emacs. +You need a recent version in either case. +
++The aim of the Proof General project is to provide a powerful and +configurable interfaces which help user-interaction with interactive +proof assistants. The strategy of Proof General is to target power +users rather than novices, but we include general user interface +niceties, such as toolbar and menus, which make use easier for all. +
+To read more about what Proof General +provides, +. +To see what Proof General looks like in use, have a look at these +screenshots. +To download Proof General, visit the +. +To contact the developers, click +. +
+ + + ++Proof General comes ready-customized for several proof assistants, +including: +
+ +| + ","The Coq Home Page") ?> + | +
+ for
+
+ +
+ First crafted by
+ Healfdene Goguen.
+
+ + Contributions by Patrick Loiseleur. + + Maintained by + Pierre Courtieu. + |
+
| + ", + "The Isabelle Home Page"); ?> + | + for
+
+ +
+ Crafted and maintained by
+ David Aspinall.
+
+ + Additional maintainance, support for + Isabelle/Isar + by + Markus Wenzel. + |
+
| + ", + "The LEGO Home Page") ?> + | + for
+
+ +
+ First crafted by Thomas Kleymann
+ and
+ Dilip Sequeira.
+
+ + Maintained by + David Aspinall + and + Paul Callaghan. + |
+
| + + | + for
+
+ +
+ Crafted and maintained by
+ Christophe Raffalli
+
+ |
+
+There is also a preliminary version of +, for +HOL98. +We are seeking a volunteer from the HOL community to support +and improve this (perhaps also supporting other HOL variants). +
++Proof General is ready to be customized to new proof assistants. +It can be to get basic support working. +Full documentation on configuration is provided. +
+ + diff --git a/html/main.phtml b/html/main.phtml deleted file mode 100644 index 7844d527..00000000 --- a/html/main.phtml +++ /dev/null @@ -1,138 +0,0 @@ --Proof General is a generic interface for proof assistants, -currently based on Emacs. -It has been developed at the -LFCS -in the University of Edinburgh. -
--Proof General -works best under -XEmacs, but can also be used with -FSF GNU Emacs. -You need a recent version in either case. -
--The aim of the Proof General project is to provide a powerful and -configurable interfaces which help user-interaction with interactive -proof assistants. The strategy of Proof General is to target power -users rather than novices, but we include general user interface -niceties, such as toolbar and menus, which make use easier for all. -
-To read more about what Proof General -provides, -. -To see what Proof General looks like in use, have a look at these -screenshots. -To download Proof General, visit the -. -To contact the developers, click -. -
- - - --Proof General comes ready-customized for several proof assistants, -including: -
- -| - ","The Coq Home Page") ?> - | -
- for
-
- -
- First crafted by
- Healfdene Goguen.
-
- - Contributions by Patrick Loiseleur. - - Maintained by - Pierre Courtieu. - |
-
| - ", - "The Isabelle Home Page"); ?> - | - for
-
- -
- Crafted and maintained by
- David Aspinall.
-
- - Additional maintainance, support for - Isabelle/Isar - by - Markus Wenzel. - |
-
| - ", - "The LEGO Home Page") ?> - | - for
-
- -
- First crafted by Thomas Kleymann
- and
- Dilip Sequeira.
-
- - Maintained by - David Aspinall - and - Paul Callaghan. - |
-
| - - | - for
-
- -
- Crafted and maintained by
- Christophe Raffalli
-
- |
-
-There is also a preliminary version of -, for -HOL98. -We are seeking a volunteer from the HOL community to support -and improve this (perhaps also supporting other HOL variants). -
--Proof General is ready to be customized to new proof assistants. -It can be to get basic support working. -Full documentation on configuration is provided. -
- - diff --git a/html/mission.html b/html/mission.html new file mode 100644 index 00000000..deec79dc --- /dev/null +++ b/html/mission.html @@ -0,0 +1,136 @@ + + ++We seek to provide an interface suite for helping users interact with +proof assistants. +
+ ++Our approach is based on these principles: +
+Above all, we take a pragmatic approach to constructing +interfaces. Our primary aim is to provide a tool which is +immediately useful for proof engineering. +
++This aim means that we harness a range of +proven techniques +reimplemented in our generic system. +Nevertheless, by the act of constructing Proof General, we do invent +and incorporate some novel advances which +contribute to research in the field. +
+ ++
+-We seek to provide an interface suite for helping users interact with -proof assistants. -
- --Our approach is based on these principles: -
-Above all, we take a pragmatic approach to constructing -interfaces. Our primary aim is to provide a tool which is -immediately useful for proof engineering. -
--This aim means that we harness a range of -proven techniques -reimplemented in our generic system. -Nevertheless, by the act of constructing Proof General, we do invent -and incorporate some novel advances which -contribute to research in the field. -
- --
-+Final week of testing for Proof General 3.2. +The last chance to report bugs or request (minor) improvements for this release. +Please help us by trying out the +pre-release, especially if you are +relying on an older or non-standard Emacs version. +Also check to see if the new +manuals are useful: now split into +the user manual in +, + +or +, +and the separate "adapting" manual, in +, + +or +. +(Info files are included in the distribution). +
++Improvements to web pages. Graphics made smaller, text more concise. +Please +for further improvements. +(I know some pages display poorly in Netscape 4.7x because +of patchy stylesheet support; they appear much better in IE5 +or the rather impressive recent versions of KDE's Konqueror). +
++We're starting the testing phase for Proof General 3.2. +It has several new features and improvements. +Please try out the pre-release +version, and report any problems to us. Your +feedback is very important because we have no resources available for +serious compatibility testing ourselves. +
++We hope to release 3.2 by the end of September. +
+
+
+
+
+News items by David Aspinall.
+
+Click here for old news.
+
-Final week of testing for Proof General 3.2. -The last chance to report bugs or request (minor) improvements for this release. -Please help us by trying out the -pre-release, especially if you are -relying on an older or non-standard Emacs version. -Also check to see if the new -manuals are useful: now split into -the user manual in -, - -or -, -and the separate "adapting" manual, in -, - -or -. -(Info files are included in the distribution). -
--Improvements to web pages. Graphics made smaller, text more concise. -Please -for further improvements. -(I know some pages display poorly in Netscape 4.7x because -of patchy stylesheet support; they appear much better in IE5 -or the rather impressive recent versions of KDE's Konqueror). -
--We're starting the testing phase for Proof General 3.2. -It has several new features and improvements. -Please try out the pre-release -version, and report any problems to us. Your -feedback is very important because we have no resources available for -serious compatibility testing ourselves. -
--We hope to release 3.2 by the end of September. -
-
-
-
-
-News items by David Aspinall.
-
-Click here for old news.
-
+Minor patch 3.1.6 released today. This turns off toolbar enablers if +you're running XEmacs on Solaris; because of strange Solaris problems, +buttons are disabled too often there. (You can live without +this part of the patch by customizing the variable +proof-toolbar-use-button-enablers). +The patch also removes +the use of an "interval timer" when +proof-toolbar-use-button-enablers is off, since a user +reported being unable to start itimers unless +running as root (likely an operating system configuration problem). +Thanks to Markus Wenzel and Pierre Lescanne for reporting problems. +
++New! For developers, a web-browsable +mirror of the Proof General cvs is available +here. +
++New! +Proof General . +Please send questions or suggestions for inclusion to +proofgen@dcs.ed.ac.uk, +thanks. +
++A minor patch to Proof General 3.1 is released today. To check what +version you have, look at the variable proof-general-version +set in proof-site.el. (It is not recorded in the tar file +name or package version). The current patch, to 3.1.4, was made to +fix a problem with Isabelle and theory file retraction, accidently +introduced in 3.1. See for details. +NB: This patch was first made on 4th April, but didn't quite solve the +problem. Thanks to Mike Squire for sending a patch to fix the fix. +
++Further improvements are being introduced in the new 3.2 pre-releases, +see the +development download page, as usual. +
++Proof General 3.1 is now available from the +. Enjoy! +
++Release candidate for Proof General 3.1 available. +Pre-releases from now on are release candidates for version 3.1. +Please test and report any problems you find +(check the CHANGES and BUGS lists for issues known about +and/or resolved). Version 3.1 should be released next week. +
++New: HOL Proof General! +It took me only a couple of hours to add a basic instantiation of +ProofGeneral for +HOL98. +Most of this time was in trying to find out how to do things in HOL, +I could have done with a HOL user to hand. But I thought it was high time +HOL got a look-in. +
++HOL Proof General provides script management support, automatic +multiple files, decoration of proof scripts and output. +Character-sequence X Symbols as in Coq and LEGO. Although this is a +basic feature set for Proof General, the result is still an enormous +improvement over shell interaction. +
++My hope is to entice HOL users so that one of them may improve HOL +Proof General. I don't plan to maintain or seriously improve this +instantiation myself. +
++The HOL support is shipping in the +current development release. +
++There is now a new +. +I plan to apply for funding to continue managing the evolution +and development of Proof General, once my own job position +is more secure. +Now is the time to flesh out ideas +for the future! +Check the development page for the +latest proposals. These include some desirable contributions +which could be undertaken as self-contained projects. +
++Countdown to Proof General 3.1 begins. This will be a bug fix releaase. +A few bugs have been fixed in +recent Proof General development releases, one important one is fixing +support for non-mule versions of FSF Emacs (thanks to Pierre Courtieu +for raising it to my attention). I would like to release PG 3.1 next +month so that everyone can benefit. +
++In the meantime, please + +that you would like to see fixed, and consider trying out +the current development release. +
++I'm pleased to say that Proof General will be demonstrated at +ETAPS 2000. +Here are some draft slides for +the presentation +(any comments would be welcome). +A presentation of Proof General based on these slides was given at +Rutherford Appleton Laboratory last week. +
++Proof General 3.0 is released! +
++Proof General 3.0 is currently in final testing, and will be released +in a small number of days. Please help me with this by testing the +current pre-release, so I can iron out as +many bugs as possible before making the release. It's very easy to +install or upgrade Proof General, so it shouldn't be much effort to +test it quickly. Particularly if you're already running an earlier +version. +
++New! With Proof General 3.0, adapting to a new prover is easier +than ever before! +It includes an + +of Proof General for Isabelle, which +configures the main core of the interface with less than 30 lines of +code. Not bad for getting about 4000 lines worth of code in benefit! +
++Isabelle 99 was released last week, and Proof General 3.0 should +be ready for release in the next week or so. In +the meantime, please use the current +pre-release +for Isabelle 99. +
++Some recent changes have been made to the support for +X-Symbol, +so that it is easier to turn on and off, and support is now +properly generic. At the moment only Isabelle has +support implemented. +
++ See what Proof General 3.0 will look like! + The screenshot has been updated. +
++ The next version of Proof General will be 3.0. +
++ There have been significant changes to the core of + Proof General and many improvements in the code. + Extra features have been added, and the ones already + there improved upon. Usability has been a particular + focus. Adding new provers has been made easier. + Installation will be made even easier. + All of these changes warrant moving to a major release! +
++ Version 3.0 is planned for release in November. + Please test a Version 3.0 pre-release if you can + and report any problems. +
+
+ I'm very grateful to
+ Pierre Courtieu <courtieu@lri.fr>
+ for offering to help work on Coq Proof General.
+
+ If anyone else in the Coq community would like to assist, please
+ offer still,
+ there is plenty to do to add: better recognition of proof scripts,
+ multiple file management, proof by pointing, etc...
+
+ Recently there has been a flurry of work on the next version of Proof
+ General. It has quite a number of improvements (see the file), made by myself
+ and Markus Wenzel.
The next version is aimed to coincide
+ roughly with the release of Isabelle 99.
+
+ At the moment we urgently need somebody from the Coq world to + maintain and improve Coq Proof General, since Patrick Loiseleur + can no longer work on it. + Support from the Coq community is vital for Proof General to + be a useful tool there. Please offer to help, + it needn't be a heavy commitment. +
+
+ I've just returned from the
+ Types Summer School, Giens, France
+ where Proof General was used for a class of
+ about 50 students who were learning
+ Coq, Isabelle, and LEGO. I received
+ many useful comments and feedback,
+ which will be
+ used to improve the next version.
+ Thanks to everyone who gave suggestions and bug reports
+ to me, including:
+ Michael Abbott,
+ Bernd Grobauer,
+ Sebastian Skalberg,
+ Thierry Massart,
+ Darmalingum Muthiayen.
+
+
+ Print pictures from the new + gallery + of publicity shots of Proof General! +
+
+ Proof General version 2.1 is released.
+
+ Check the file
+ for a summary of changes since Proof General 2.0.
+
+ It is recommended that all users upgrade except
+ those still using Isabelle 98-1.
+
+ Proof General 2.1 supports only the 99 version of Isabelle.
+
+ New Proof General web pages go live! +
++ The general is now more serious looking. + Appropriate, because there are some serious improvements + in the pipeline... + Before that, we will release Proof General 2.1, + mainly a bug-fix improvement of 2.0. +
++ Please explore the new web pages and report any problems + or suggestions to . + Please also try out the latest pre-release of Proof General, + this is the final chance to get fixes and tweaks + sorted before 2.1. +
+A new instantiation of Proof General has been added by + Paul Callaghan + for + Plastic, + a new proof assistant based on + Luo's Typed Logical Framework and + implemented in Haskell. +
+A new instantiation of Proof General has been added by + Markus Wenzel + for Isabelle/Isar, + a new proof language for Isabelle to be included with Isabelle 99. +
++News items by David Aspinall. +
+ + + diff --git a/html/oldnews.phtml b/html/oldnews.phtml deleted file mode 100644 index 4078fd73..00000000 --- a/html/oldnews.phtml +++ /dev/null @@ -1,309 +0,0 @@ - --Minor patch 3.1.6 released today. This turns off toolbar enablers if -you're running XEmacs on Solaris; because of strange Solaris problems, -buttons are disabled too often there. (You can live without -this part of the patch by customizing the variable -proof-toolbar-use-button-enablers). -The patch also removes -the use of an "interval timer" when -proof-toolbar-use-button-enablers is off, since a user -reported being unable to start itimers unless -running as root (likely an operating system configuration problem). -Thanks to Markus Wenzel and Pierre Lescanne for reporting problems. -
--New! For developers, a web-browsable -mirror of the Proof General cvs is available -here. -
--New! -Proof General . -Please send questions or suggestions for inclusion to -proofgen@dcs.ed.ac.uk, -thanks. -
--A minor patch to Proof General 3.1 is released today. To check what -version you have, look at the variable proof-general-version -set in proof-site.el. (It is not recorded in the tar file -name or package version). The current patch, to 3.1.4, was made to -fix a problem with Isabelle and theory file retraction, accidently -introduced in 3.1. See for details. -NB: This patch was first made on 4th April, but didn't quite solve the -problem. Thanks to Mike Squire for sending a patch to fix the fix. -
--Further improvements are being introduced in the new 3.2 pre-releases, -see the -development download page, as usual. -
--Proof General 3.1 is now available from the -. Enjoy! -
--Release candidate for Proof General 3.1 available. -Pre-releases from now on are release candidates for version 3.1. -Please test and report any problems you find -(check the CHANGES and BUGS lists for issues known about -and/or resolved). Version 3.1 should be released next week. -
--New: HOL Proof General! -It took me only a couple of hours to add a basic instantiation of -ProofGeneral for -HOL98. -Most of this time was in trying to find out how to do things in HOL, -I could have done with a HOL user to hand. But I thought it was high time -HOL got a look-in. -
--HOL Proof General provides script management support, automatic -multiple files, decoration of proof scripts and output. -Character-sequence X Symbols as in Coq and LEGO. Although this is a -basic feature set for Proof General, the result is still an enormous -improvement over shell interaction. -
--My hope is to entice HOL users so that one of them may improve HOL -Proof General. I don't plan to maintain or seriously improve this -instantiation myself. -
--The HOL support is shipping in the -current development release. -
--There is now a new -. -I plan to apply for funding to continue managing the evolution -and development of Proof General, once my own job position -is more secure. -Now is the time to flesh out ideas -for the future! -Check the development page for the -latest proposals. These include some desirable contributions -which could be undertaken as self-contained projects. -
--Countdown to Proof General 3.1 begins. This will be a bug fix releaase. -A few bugs have been fixed in -recent Proof General development releases, one important one is fixing -support for non-mule versions of FSF Emacs (thanks to Pierre Courtieu -for raising it to my attention). I would like to release PG 3.1 next -month so that everyone can benefit. -
--In the meantime, please - -that you would like to see fixed, and consider trying out -the current development release. -
--I'm pleased to say that Proof General will be demonstrated at -ETAPS 2000. -Here are some draft slides for -the presentation -(any comments would be welcome). -A presentation of Proof General based on these slides was given at -Rutherford Appleton Laboratory last week. -
--Proof General 3.0 is released! -
--Proof General 3.0 is currently in final testing, and will be released -in a small number of days. Please help me with this by testing the -current pre-release, so I can iron out as -many bugs as possible before making the release. It's very easy to -install or upgrade Proof General, so it shouldn't be much effort to -test it quickly. Particularly if you're already running an earlier -version. -
--New! With Proof General 3.0, adapting to a new prover is easier -than ever before! -It includes an - -of Proof General for Isabelle, which -configures the main core of the interface with less than 30 lines of -code. Not bad for getting about 4000 lines worth of code in benefit! -
--Isabelle 99 was released last week, and Proof General 3.0 should -be ready for release in the next week or so. In -the meantime, please use the current -pre-release -for Isabelle 99. -
--Some recent changes have been made to the support for -X-Symbol, -so that it is easier to turn on and off, and support is now -properly generic. At the moment only Isabelle has -support implemented. -
-- See what Proof General 3.0 will look like! - The screenshot has been updated. -
-- The next version of Proof General will be 3.0. -
-- There have been significant changes to the core of - Proof General and many improvements in the code. - Extra features have been added, and the ones already - there improved upon. Usability has been a particular - focus. Adding new provers has been made easier. - Installation will be made even easier. - All of these changes warrant moving to a major release! -
-- Version 3.0 is planned for release in November. - Please test a Version 3.0 pre-release if you can - and report any problems. -
-
- I'm very grateful to
- Pierre Courtieu <courtieu@lri.fr>
- for offering to help work on Coq Proof General.
-
- If anyone else in the Coq community would like to assist, please
- offer still,
- there is plenty to do to add: better recognition of proof scripts,
- multiple file management, proof by pointing, etc...
-
- Recently there has been a flurry of work on the next version of Proof
- General. It has quite a number of improvements (see the file), made by myself
- and Markus Wenzel.
The next version is aimed to coincide
- roughly with the release of Isabelle 99.
-
- At the moment we urgently need somebody from the Coq world to - maintain and improve Coq Proof General, since Patrick Loiseleur - can no longer work on it. - Support from the Coq community is vital for Proof General to - be a useful tool there. Please offer to help, - it needn't be a heavy commitment. -
-
- I've just returned from the
- Types Summer School, Giens, France
- where Proof General was used for a class of
- about 50 students who were learning
- Coq, Isabelle, and LEGO. I received
- many useful comments and feedback,
- which will be
- used to improve the next version.
- Thanks to everyone who gave suggestions and bug reports
- to me, including:
- Michael Abbott,
- Bernd Grobauer,
- Sebastian Skalberg,
- Thierry Massart,
- Darmalingum Muthiayen.
-
-
- Print pictures from the new - gallery - of publicity shots of Proof General! -
-
- Proof General version 2.1 is released.
-
- Check the file
- for a summary of changes since Proof General 2.0.
-
- It is recommended that all users upgrade except
- those still using Isabelle 98-1.
-
- Proof General 2.1 supports only the 99 version of Isabelle.
-
- New Proof General web pages go live! -
-- The general is now more serious looking. - Appropriate, because there are some serious improvements - in the pipeline... - Before that, we will release Proof General 2.1, - mainly a bug-fix improvement of 2.0. -
-- Please explore the new web pages and report any problems - or suggestions to . - Please also try out the latest pre-release of Proof General, - this is the final chance to get fixes and tweaks - sorted before 2.1. -
-A new instantiation of Proof General has been added by - Paul Callaghan - for - Plastic, - a new proof assistant based on - Luo's Typed Logical Framework and - implemented in Haskell. -
-A new instantiation of Proof General has been added by - Markus Wenzel - for Isabelle/Isar, - a new proof language for Isabelle to be included with Isabelle 99. -
--News items by David Aspinall. -
- - - diff --git a/html/oldrel.html b/html/oldrel.html new file mode 100644 index 00000000..9aa952ff --- /dev/null +++ b/html/oldrel.html @@ -0,0 +1,112 @@ + + ++Please note that we do not support these old releases in any way. +
+ ++This version of Proof General has been tested +with XEmacs 21.1 and FSF Emacs 20.4. +It supports Coq version 6.3, LEGO version 1.3.1 and +Isabelle99. +
+ ++Check the file +for a summary of changes since version 3.0. +
+ + + +
+This version of Proof General has been tested
+with XEmacs 20.4, XEmacs 21.1.8 and FSF Emacs 20.5.
+It supports Coq version 6.3, LEGO version 1.3.1 and Isabelle99.
+
+Check the file +for a summary of changes since version 2.1. +
+ + + +
+This version of Proof General has been tested
+with XEmacs 20.4, XEmacs 21 and FSF Emacs 20.3.
+It supports Coq version 6.3, LEGO version 1.3.1 and
+some pre-release versions of Isabelle version 99.
+
+Check the file +for a summary of changes since version 2.0. +
+ + +
+This version of Proof General has been tested
+with XEmacs 20.4 and FSF Emacs 20.2, 20.3.
+It supports Coq version 6.2, LEGO version 1.3.1, and
+Isabelle version 98-1.
+
-Please note that we do not support these old releases in any way. -
- --This version of Proof General has been tested -with XEmacs 21.1 and FSF Emacs 20.4. -It supports Coq version 6.3, LEGO version 1.3.1 and -Isabelle99. -
- --Check the file -for a summary of changes since version 3.0. -
- - - -
-This version of Proof General has been tested
-with XEmacs 20.4, XEmacs 21.1.8 and FSF Emacs 20.5.
-It supports Coq version 6.3, LEGO version 1.3.1 and Isabelle99.
-
-Check the file -for a summary of changes since version 2.1. -
- - - -
-This version of Proof General has been tested
-with XEmacs 20.4, XEmacs 21 and FSF Emacs 20.3.
-It supports Coq version 6.3, LEGO version 1.3.1 and
-some pre-release versions of Isabelle version 99.
-
-Check the file -for a summary of changes since version 2.0. -
- - -
-This version of Proof General has been tested
-with XEmacs 20.4 and FSF Emacs 20.2, 20.3.
-It supports Coq version 6.2, LEGO version 1.3.1, and
-Isabelle version 98-1.
-
+Here are some proposals for projects connected to Proof General. +
++The projects are designed as fairly self-contained contributions, +involving code development and possibly a portion of supporting +research. They would be ideal projects for interested students +or researchers. +
++The projects are divided into those which are specific to Proof +General, and those which would be useful more widely and do not depend +on Proof General. For more information on a project, click on its +title. +
+ ++Some projects involve Emacs Lisp. This is the embedded programming +language inside Emacs. It is very easy to learn, since it is small, +has a good manual, and has an interactive interpreter. It is easy to +use, not least because of its self-documenting nature: each +variable or function is compiled together with documentation of its +purpose. (Other languages would do well to follow this). It also +has a powerful source-level debugger, edebug. +
+ + + + + + + + + + + + ++If you are interested in working on any of these projects, +feel free to discuss with the project proposer or on the +. +
+ ++If you would like to use any of these ideas as a formal project +proposal for students at your institution, please feel free +but do +if some work is begun, to help coordinate efforts. +NB: the proposer of the project does not guarantee to be available for +formal supervision or intensive help with the project (but it may be +possible to find somebody else to do that). +
+ ++If you would like to submit a project proposal +for an improvement or extension of Proof General, +please send an email or write a description on the +. +Projects should be significant contributions rather than +incremental improvements (although we welcome the suggestion of those +too). +
+ + + diff --git a/html/projects.phtml b/html/projects.phtml deleted file mode 100644 index a8c180aa..00000000 --- a/html/projects.phtml +++ /dev/null @@ -1,96 +0,0 @@ - - --Here are some proposals for projects connected to Proof General. -
--The projects are designed as fairly self-contained contributions, -involving code development and possibly a portion of supporting -research. They would be ideal projects for interested students -or researchers. -
--The projects are divided into those which are specific to Proof -General, and those which would be useful more widely and do not depend -on Proof General. For more information on a project, click on its -title. -
- --Some projects involve Emacs Lisp. This is the embedded programming -language inside Emacs. It is very easy to learn, since it is small, -has a good manual, and has an interactive interpreter. It is easy to -use, not least because of its self-documenting nature: each -variable or function is compiled together with documentation of its -purpose. (Other languages would do well to follow this). It also -has a powerful source-level debugger, edebug. -
- - - - - - - - - - - - --If you are interested in working on any of these projects, -feel free to discuss with the project proposer or on the -. -
- --If you would like to use any of these ideas as a formal project -proposal for students at your institution, please feel free -but do -if some work is begun, to help coordinate efforts. -NB: the proposer of the project does not guarantee to be available for -formal supervision or intensive help with the project (but it may be -possible to find somebody else to do that). -
- --If you would like to submit a project proposal -for an improvement or extension of Proof General, -please send an email or write a description on the -. -Projects should be significant contributions rather than -incremental improvements (although we welcome the suggestion of those -too). -
- - - diff --git a/html/register.html b/html/register.html new file mode 100644 index 00000000..4390ef83 --- /dev/null +++ b/html/register.html @@ -0,0 +1,110 @@ + ++ Your registration form was incomplete. Please fill in all + the fields, thank-you! +
+ +
+Please register your download using the short form below.
+
+The information provided will only be used to help
+provide a case for support for Proof General in the future.
+
+If you have already registered you do not need to fill in the form +again, so return to +
+ ++
+Dear " . $name . ",\n"; + print "";
+ print "Thank you for filling in the form. Your registration has been sent.
";
+
+ /* Next bit duplicated in mailinglist.phtml.
+ Could be a function in functions.php3 */
+
+ if ($mailinglist) {
+ $message = "subscribe proofgeneral";
+ mail("majordomo@dcs.ed.ac.uk",
+ "[Web form from ~proofgen]",
+ $message,
+ "Reply-To: " . $email . "\nFrom: " . $email);
+ print "Your name has been added to the Proof General mailing list.
";
+ }
+ print "
"; + + print "
\nClick ";
+ link_root("download#prereq","here");
+ print " to return to the download page.
- Your registration form was incomplete. Please fill in all - the fields, thank-you! -
- -
-Please register your download using the short form below.
-
-The information provided will only be used to help
-provide a case for support for Proof General in the future.
-
-If you have already registered you do not need to fill in the form -again, so return to -
- --
-Dear " . $name . ",\n"; - print "";
- print "Thank you for filling in the form. Your registration has been sent.
";
-
- /* Next bit duplicated in mailinglist.phtml.
- Could be a function in functions.php3 */
-
- if ($mailinglist) {
- $message = "subscribe proofgeneral";
- mail("majordomo@dcs.ed.ac.uk",
- "[Web form from ~proofgen]",
- $message,
- "Reply-To: " . $email . "\nFrom: " . $email);
- print "Your name has been added to the Proof General mailing list.
";
- }
- print "
"; - - print "
\nClick ";
- link_root("download#prereq","here");
- print " to return to the download page.
+Here are some screenshots of Proof General 3.0 running with +different theorem provers. To see the full-size version +of a picture, click on its thumbnail. +
++NB: Your browser needs PNG support to view these pictures. + +
+ + +
+
+
+
+ |
+
+
+Building a simple proof in LEGO with proof-by-pointing.
+ |
+
+
+
+ |
+
+
+Coq Proof General running in multiple frame mode,
+full screen shot (1024x768).
+ |
+
+
+
+ |
+
+
+Replaying a domain theory proof in Isabelle's HOLCF logic.
+ |
+
+
+
+ |
+
+ +Replaying a proof in Isar, Isabelle's new proof language +developed by Markus Wenzel. + + |
+
+
+
+ |
+
+
+LEGO Proof General running in plain console mode.
+ |
+For more pictures, see the Proof General gallery. +
+ diff --git a/html/screenshot.phtml b/html/screenshot.phtml deleted file mode 100644 index b57c0d37..00000000 --- a/html/screenshot.phtml +++ /dev/null @@ -1,108 +0,0 @@ --Here are some screenshots of Proof General 3.0 running with -different theorem provers. To see the full-size version -of a picture, click on its thumbnail. -
--NB: Your browser needs PNG support to view these pictures. - -
- - -|
-
-
-
- |
-
-
-Building a simple proof in LEGO with proof-by-pointing.
- |
|
-
-
-
- |
-
-
-Coq Proof General running in multiple frame mode,
-full screen shot (1024x768).
- |
|
-
-
-
- |
-
-
-Replaying a domain theory proof in Isabelle's HOLCF logic.
- |
|
-
-
-
- |
-
- -Replaying a proof in Isar, Isabelle's new proof language -developed by Markus Wenzel. - - |
|
-
-
-
- |
-
-
-LEGO Proof General running in plain console mode.
- |
-For more pictures, see the Proof General gallery. -
- diff --git a/html/smallheader.html b/html/smallheader.html new file mode 100644 index 00000000..8cf93a42 --- /dev/null +++ b/html/smallheader.html @@ -0,0 +1,8 @@ +
+
+
+
+ |
+
diff --git a/html/smallheader.phtml b/html/smallheader.phtml
deleted file mode 100644
index 8cf93a42..00000000
--- a/html/smallheader.phtml
+++ /dev/null
@@ -1,8 +0,0 @@
-
|