# HG changeset patch # User haftmann # Date 1193482124 -7200 # Node ID 91730b492a45152edcbb998fe1dc2147c53f4324 # Parent 48a1e80f5cdb384e4cb58b713b5411ec1900e561 ASCIIfied README diff -r 48a1e80f5cdb -r 91730b492a45 Admin/CHECKLIST --- a/Admin/CHECKLIST Sat Oct 27 12:48:24 2007 +0200 +++ b/Admin/CHECKLIST Sat Oct 27 12:48:44 2007 +0200 @@ -3,7 +3,7 @@ - Admin/update-keywords; -- check ANNOUNCE, README.html, INSTALL, NEWS, COPYRIGHT, CONTRIBUTORS, ~isabelle/website; +- check ANNOUNCE, README, INSTALL, NEWS, COPYRIGHT, CONTRIBUTORS, ~isabelle/website; - run tests with all supported ML systems; @@ -21,7 +21,7 @@ Doc/Logics/logics.tex - after release: - commit new ~isabelle/website/include/documentationdist.include.html to CVS + commit new ~isabelle/website/include/documentationdist.include.html to website SVN !!! commit new Admin/website/conf/distname.mak to CVS !!! this is currently not part of CVS, so ignore this description; !!! perhaps we will need to add it diff -r 48a1e80f5cdb -r 91730b492a45 Admin/makedist --- a/Admin/makedist Sat Oct 27 12:48:24 2007 +0200 +++ b/Admin/makedist Sat Oct 27 12:48:44 2007 +0200 @@ -46,7 +46,7 @@ * Symlink website to Admin/website * Check Admin/website contents. - * Check ANNOUNCE, README.html, INSTALL, NEWS, COPYRIGHT, CONTRIBUTORS. + * Check ANNOUNCE, README, INSTALL, NEWS, COPYRIGHT, CONTRIBUTORS. * Try "isatool makeall all" with Poly/ML, SML/NJ, etc. * Tag the current repository version, e.g.: cvs -d /usr/proj/isabelle-repository/archive rtag IsabelleXXXX isabelle @@ -192,8 +192,7 @@ perl -pi -e "s/{ISABELLE}/$DISTNAME/g;" lib/html/index.html perl -pi -e "s/Isabelle repository version/$DISTVERSION/" src/Pure/ROOT.ML lib/Tools/version -perl -pi -e "s/the internal repository version of Isabelle/$DISTVERSION/" README.html -lynx -dump README.html >README +perl -pi -e "s/the internal repository version of Isabelle/$DISTVERSION/" README ( cd src; ../Admin/maketags; ) @@ -241,7 +240,7 @@ mv "$DISTNAME" "${DISTNAME}-old" mkdir "$DISTNAME" -mv "${DISTNAME}-old/README.html" "${DISTNAME}-old/INSTALL" "${DISTNAME}-old/NEWS" \ +mv "${DISTNAME}-old/README" "${DISTNAME}-old/INSTALL" "${DISTNAME}-old/NEWS" \ "${DISTNAME}-old/ANNOUNCE" "${DISTNAME}-old/COPYRIGHT" "${DISTNAME}-old/CONTRIBUTORS" \ "$DISTNAME" mkdir "$DISTNAME/doc" diff -r 48a1e80f5cdb -r 91730b492a45 README --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/README Sat Oct 27 12:48:44 2007 +0200 @@ -0,0 +1,87 @@ + The Isabelle System Distribution + +Version information + + This is the internal repository version of Isabelle. See the NEWS file + in the distribution for details on user-relevant changes. + +System requirements + + Isabelle requires a regular Unix platform (e.g. GNU Linux) with the + following additional software: + * A full Standard ML Compiler (e.g. Poly/ML 5.x, 4.x). + * The GNU bash shell (version 3.x, 2.x). + * Perl (version 5.x). + * XEmacs (version 21.4.x) -- for the ProofGeneral interface. + * A complete LaTeX installation -- for document preparation. + +Installation + + Binary packages are available for Isabelle/HOL and ZF for several + platforms from the Isabelle web page. The system may be easily built + from scratch as well, taking the traditional tar.gz source + distribution. See file INSTALL as distributed with Isabelle for more + information. + + Further background information may be found in the Isabelle System + Manual, distributed with the sources (directory doc). + +User interface + + The canonical Isabelle user interface is [1]Proof General by David + Aspinall and others. It is a generic (X)Emacs interface for proof + assistants, including Isabelle (both for the classic and Isar + version). Proof General is suitable for use by pacifists and Emacs + militants alike. Its most prominent feature is script management, + providing a metaphor of live proof script editing. Proof General has + recently gained a rather large following of both beginning and expert + users of Isabelle. + + Proof General is distributed together with the XEmacs [2]X-Symbol + package, which provides a nice way to get proper mathematical symbols + displayed on screen. + +Other sources of information + + The Isabelle Page + + The Isabelle home page may be accessed both from Cambridge and Munich: + * [3]http://www.cl.cam.ac.uk/Research/HVG/Isabelle/ + * [4]http://isabelle.in.tum.de + + Mailing list + + The electronic mailing list isabelle-users@cl.cam.ac.uk provides a + forum for Isabelle users to discuss problems and exchange information. + To join, send a message to [5]isabelle-users-request@cl.cam.ac.uk. + + Personal mail + + [6]Lawrence C Paulson + Computer Laboratory + University of Cambridge + JJ Thomson Avenue + Cambridge CB3 0FD + England + E-mail: [7]lcp@cl.cam.ac.uk + Phone: +44-223-763500 + Fax: +44-223-334748 + + or + + [8]Tobias Nipkow + Institut für Informatik + Technische Universität München + Boltzmannstr. 3 + D-85748 Garching + Germany + E-mail: [9]nipkow@in.tum.de + Phone: +49-89-289-17302 + Fax: +49-89-289-17307 + _________________________________________________________________ + + Please report any problems you encounter. While we shall try to be + helpful, we can accept no responsibility for the deficiencies of + Isabelle and their consequences. + _________________________________________________________________ + diff -r 48a1e80f5cdb -r 91730b492a45 README.html --- a/README.html Sat Oct 27 12:48:24 2007 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,121 +0,0 @@ - - - - - - - - - The Isabelle System Distribution - - - - -

The Isabelle System Distribution

- -

Version information

- -

This is the internal repository version of Isabelle. See the -NEWS file in the distribution for details on user-relevant -changes.

- -

System requirements

- -

Isabelle requires a regular Unix platform (e.g. GNU Linux) with the -following additional software:

- - - -

Installation

- -

Binary packages are available for Isabelle/HOL and ZF for several -platforms from the Isabelle web page. The system may be easily built -from scratch as well, taking the traditional tar.gz source -distribution. See file INSTALL as distributed with Isabelle -for more information.

- -

Further background information may be found in the Isabelle System -Manual, distributed with the sources (directory doc).

- -

User interface

- -

The canonical Isabelle user interface is Proof General by David Aspinall -and others. It is a generic (X)Emacs interface for proof assistants, -including Isabelle (both for the classic and Isar version). Proof -General is suitable for use by pacifists and Emacs militants -alike. Its most prominent feature is script management, providing a -metaphor of live proof script editing. Proof General has -recently gained a rather large following of both beginning and expert -users of Isabelle.

- -

Proof General is distributed together with the XEmacs - -X-Symbol package, which provides a nice way to get proper -mathematical symbols displayed on screen.

- -

Other sources of information

- -

The Isabelle Page

- -

The Isabelle home page may be accessed both from Cambridge and Munich:

- - - - -

Mailing list

- -

The electronic mailing list isabelle-users@cl.cam.ac.uk -provides a forum for Isabelle users to discuss problems and exchange -information. To join, send a message to isabelle-users-request@cl.cam.ac.uk.

- - -

Personal mail

- -Lawrence C Paulson
-Computer Laboratory
-University of Cambridge
-JJ Thomson Avenue
-Cambridge CB3 0FD
-England
-
-E-mail: lcp@cl.cam.ac.uk
-Phone: +44-223-763500
-Fax: +44-223-334748
- -

-or -

- -Tobias Nipkow
-Institut für Informatik
-Technische Universität München
-Boltzmannstr. 3
-D-85748 Garching
-Germany
-
-E-mail: nipkow@in.tum.de
-Phone: +49-89-289-17302
-Fax: +49-89-289-17307
-

- -

- -Please report any problems you encounter. While we shall try to be -helpful, we can accept no responsibility for the deficiencies of -Isabelle and their consequences. - -
- - -