+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/index.html b/html/index.html new file mode 100644 index 00000000..f0cbe7a1 --- /dev/null +++ b/html/index.html @@ -0,0 +1,9 @@ + + + + + -- cgit v1.2.3
+ cd ~/.xemacs
+ tar xpzf ../x-symbol-pkg.tar.gz
+