From bd7aa7923a25d16207842f9f3d6b773c2fc6fa58 Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Thu, 28 Sep 2000 15:01:50 +0000 Subject: Renamed file --- html/main.html | 138 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 138 insertions(+) create mode 100644 html/main.html (limited to 'html/main.html') 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 @@ +

What is Proof General?

+

+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 +. +

+ + + +

What systems does Proof General work with?

+

+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. +

+ + -- cgit v1.2.3