Ideas for the future of Proof General are given here:
-
-
- David Aspinall. +
- David Aspinall. Protocols for Interactive e-Proof. Draft version, see - here. + here.
- David Aspinall.
Proof General Kit (white paper).
diff --git a/html/feedback.phtml b/html/feedback.phtml
index 6413f83b..17dc974c 100644
--- a/html/feedback.phtml
+++ b/html/feedback.phtml
@@ -21,8 +21,8 @@ or offers to help with Proof Generl development.
Or send email directly to the -Proof General maintainer -<proofgen@dcs.ed.ac.uk>. +Proof General maintainer +<feedback@proofgeneral.org>.You can also report a bug using this form, although it would @@ -77,7 +77,7 @@ Dear Proof General developers, 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("da", /*"proofgen@dcs.ed.ac.uk",*/ + mail("feedback@proofgeneral.org", "[Web Feedback Form]: " . $subject, $message, "Reply-To: " . $from . "\n"); diff --git a/html/footer.phtml b/html/footer.phtml index 99af0885..9fd59285 100644 --- a/html/footer.phtml +++ b/html/footer.phtml @@ -7,9 +7,9 @@ Web pages by -David Aspinall. +David Aspinall.
Contact -Proof General maintainer. +Proof General maintainer.
\ No newline at end of file diff --git a/html/functions.php3 b/html/functions.php3 index 0422dc37..28130564 100644 --- a/html/functions.php3 +++ b/html/functions.php3 @@ -14,8 +14,8 @@ // Project configuration -$project_email = "proofgen@dcs.ed.ac.uk"; -$project_list = "proofgeneral@dcs.ed.ac.uk"; +$project_email = "feedback@proofgeneral.org"; +$project_list = "users@proofgeneral.org"; $project_title = "Proof General"; $project_subtitle = "Organize your Proofs!"; $project_full_title = $project_title . " --- " . $project_subtitle; @@ -31,8 +31,9 @@ print $dtd_loose; // Validator address -$validator = "http://validator.dcs.ed.ac.uk/"; -// $validator = "http://localhost/validator/"; +// $validator = "http://validator.dcs.ed.ac.uk/"; +// It's a private link which won't work elsewhere, but never mind. + $validator = "http://localhost/validator/"; function mlink($addr) { print "" . $addr . ""; @@ -112,13 +113,10 @@ function date_modified($filename) { } } -/* Nav bar separator */ -$separator = '
';
-
/* A link to one of the main pages (must appear in navbar menu) */
function link_root($page,$text) {
- print "";
+ print "";
print $text;
print "";
}
diff --git a/html/header.phtml b/html/header.phtml
index cd2af8ee..e5100744 100644
--- a/html/header.phtml
+++ b/html/header.phtml
@@ -1,5 +1,5 @@
-+
\ No newline at end of file diff --git a/html/mailinglist.phtml b/html/mailinglist.phtml index dd63aafc..b6336f45 100644 --- a/html/mailinglist.phtml +++ b/html/mailinglist.phtml @@ -17,8 +17,8 @@ ?>@@ -17,20 +17,20 @@ * Look for $WANTED in array. If not found, use default of "Home" * and fix $WANTED. Hrefs are given by page parameter to current doc. */ - $separator=' ';
+ $separator='';
$WANTED=$HTTP_GET_VARS["page"];
- print "
\n"; ?> +\n"; + print "
\n"; + print "\n"; $links_arr = array( "Home" => "main", "Features" => "features", "Download" => "download", - "Documentation" => "doc", "News" => "news", + "Screenshots" => "screenshot", + "Documentation" => "doc", "Development" => "devel", "About" => "about", "Links" => "links" ); - $midpoint = $DEFAULT = $links_arr["Home"]; $wanted_okay = 0; for (reset($links_arr); $name = key($links_arr); next($links_arr)) { @@ -44,16 +44,17 @@ for (reset($links_arr); $name = key($links_arr); next($links_arr)) { print $separator; if ($WANTED == $links_arr[$name]) { - print "" . $name . ""; + print "" . $name . ""; } else { link_root($links_arr[$name],$name); } - print "\n"; - if ($name=="Download" || $name=="Development") print " "; + print " \n"; + if ($name=="Download" || $name=="Documentation") print " \n"; } - print " The mailing list address is - -proofgeneral@dcs.ed.ac.uk. + +users@proofgeneral.org.
@@ -26,8 +26,8 @@ The mailing list address is To subscribe or unsubscribe, you can fill in the form below.
Or send a message to - - majordomo@dcs.ed.ac.uk + + majordomo@proofgeneral.org with the words "subscribe proofgeneral" (or "unsubscribe proofgeneral") in the message body. @@ -37,7 +37,8 @@ with the words "subscribe proofgeneral" 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. No junk mail will be forwarded to list members. +announcements. Junk mail filters are applied to the list to +prevent junk being forwarded to list members.Mailing list subscription
diff --git a/html/main.phtml b/html/main.phtml index f0d07253..7844d527 100644 --- a/html/main.phtml +++ b/html/main.phtml @@ -13,7 +13,12 @@ works best under 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, @@ -27,7 +32,6 @@ To contact the developers, click
-What systems does Proof General work with?
@@ -50,13 +54,34 @@ including: First crafted by Healfdene Goguen.
- Later contributions by Patrick Loiseleur. + Contributions by Patrick Loiseleur.
- Maintained by - Pierre Courtieu. + Maintained by + Pierre Courtieu. ++ + ", + "The Isabelle Home Page"); ?> + +for + + +
++ Crafted and maintained by + David Aspinall. ++
+ Additional maintainance, support for + Isabelle/Isar + by + Markus Wenzel. +Dilip Sequeira.
Maintained by - David Aspinall + David Aspinall and Paul Callaghan.- - ", - "The Isabelle Home Page"); ?> + + -for - -
+for + + +
Crafted and maintained by - David Aspinall. --
- Additional maintainance, support for - Isabelle/Isar - by - Markus Wenzel. + Christophe Raffallidiff --git a/html/news.phtml b/html/news.phtml index 214fd57b..f717ad77 100644 --- a/html/news.phtml +++ b/html/news.phtml @@ -22,6 +22,7 @@ and the separate "adapting" manual, in or . (Info files are included in the distribution). +
- 14th Sep 2000
Improvements to web pages. Graphics made smaller, text more concise. diff --git a/html/screenshot.phtml b/html/screenshot.phtml index c4dc4b92..b57c0d37 100644 --- a/html/screenshot.phtml +++ b/html/screenshot.phtml @@ -1,14 +1,11 @@ -
-Here are some screenshots of Proof General running with +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) +NB: Your browser needs PNG support to view these pictures. +
@@ -108,7 +105,4 @@ graphical features are reduced!For more pictures, see the Proof General gallery.
- + diff --git a/html/smallheader.phtml b/html/smallheader.phtml index 2cb36ce3..8cf93a42 100644 --- a/html/smallheader.phtml +++ b/html/smallheader.phtml @@ -2,8 +2,7 @@- 
+
-- cgit v1.2.3