--- a/Admin/website/dist/css/isabelle_base.css Mon Jul 04 14:42:06 2005 +0200
+++ b/Admin/website/dist/css/isabelle_base.css Mon Jul 04 15:15:55 2005 +0200
@@ -105,10 +105,6 @@
border-left: 7px solid #0000A0;
}
-body.dist div#navigation ul li strong {
- border-left: 7px solid #00A000;
-}
-
/* footer layout */
div#footer p {
text-align: right;
--- a/Admin/website/dist/css/isabelle_screen.css Mon Jul 04 14:42:06 2005 +0200
+++ b/Admin/website/dist/css/isabelle_screen.css Mon Jul 04 15:15:55 2005 +0200
@@ -108,30 +108,22 @@
padding-left: 10px;
}
-body.dist div#content {
- /* not needed now */
-}
-
/* mirror switch layout */
div.mirrorlist {
- margin: 5pt 0pt 10pt 10pt;
- padding: 0pt;
- position: relative;
- float: right;
- top: 0px;
- right: 0px;
- border: 2pt solid #000000;
- background-color: #EEEEDD;
+ margin: 1ex 0em;
+ padding: 2pt;
+ background-color: #E0E0F0;
text-align: left;
+ border-left: 7px solid #FFFFFF;
}
-div.mirrorlist p {
+div.mirrorlist h3 {
margin: 1pt;
padding: 1pt;
border: none;
- background-color: #000000;
- color: #EEEEDD;
- font-size: 9pt;
+ background-color: #FFFFFF;
+ color: #0000A0;
+ font-size: 11pt;
text-align: left;
}
--- a/Admin/website/dist/documentation.html Mon Jul 04 14:42:06 2005 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,75 +0,0 @@
-<?xml version='1.0' encoding='iso-8859-1' ?>
-<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
-<!-- $Id$ -->
-<html xmlns="http://www.w3.org/1999/xhtml">
-
-<head>
- <title>Documentation</title>
- <?include file="//include/htmlheader.include.html"?>
-</head>
-
-<body class="dist">
- <?include file="//include/header.include.html"?>
- <div class="hr"><hr/></div>
- <?include file="//include/navigation_dist.include.html"?>
- <div class="hr"><hr/></div>
-
- <div id="content">
- <?include file="//include/mirrorlist.minor.include.html"?>
- <div class="hr"><hr/></div>
- <h2>Getting started</h2>
-
- <a href="//dist/img/tutorial_cover_big.gif">
- <img class="left" src="//dist/img/tutorial_cover_small.gif" alt="Cover "
- width="83" height="125"/>
- </a>
- <p>For getting started with Isabelle quickly, we recommend the <a href=
- "//dist/packages/Isabelle/doc/tutorial.pdf">Tutorial on
- Isabelle/HOL</a> (published by Springer Verlag as <a href=
- "http://www4.in.tum.de/~nipkow/LNCS2283/">LNCS 2283</a>) and the <a href=
- "#course_material">course material</a>.</p>
- <br clear="all" />
-
- <h2>Mailing list and FAQ</h2>
-
- <p>You may use the mailing list <a href=
- "mailto:isabelle-users@cl.cam.ac.uk">isabelle-users@cl.cam.ac.uk</a> and its
- <a href="http://www.cl.cam.ac.uk/users/lcp/archive/">archive</a> to discuss
- problems and results. To subscribe, <a href=
- "mailto:lcp@cl.cam.ac.uk?subject=subscribe&body=Please%20add%20me%20to%20the%20Isabelle%20mailing%20list">
- contact Larry Paulson</a>.</p>
- <p>Please consult the <a href="http://isabelle.in.tum.de/faq.html">FAQ</a> for answers to frequent
- problems.</p>
-
- <h2>Isabelle Documentation</h2>
-
- <p><?value key="distname"?> documentation is
- included here as browsable PDF for convenience. These documents are also part
- of the standard Isabelle distribution.</p>
-
- <?include file="//include/documentationdist.include.html"?>
-
- <h3>Release notes</h3>
-
- <ul>
- <li><a href="//dist/packages/Isabelle/ANNOUNCE">ANNOUNCE</a></li>
- <li><a href="//dist/packages/Isabelle/README.html">README</a></li>
- <li><a href="//dist/packages/Isabelle/INSTALL">INSTALL</a></li>
- <li><a href="//dist/packages/Isabelle/NEWS">NEWS</a></li>
- <!-- <li><a href="//dist/packages/Isabelle/COPYRIGHT">COPYRIGHT</a></li> -->
- <!-- <li><a href="//dist/packages/Isabelle/CONTRIBUTORS">CONTRIBUTORS</a></li> -->
- </ul>
-
- <h2 id="course_material">Course Material and Exercises</h2>
- <p>The <a href=
- "http://isabelle.in.tum.de/coursematerial/">course material</a> page makes
- slides, demos, and exercises of a growing number of Isabelle courses
- available. It is meant as a resource for people who would like to learn
- Isabelle as well as for those who would like to teach it.</p>
-
- </div>
- <div class="hr"><hr/></div>
- <?include file="//include/footer.include.html"?>
-</body>
-
-</html>
--- a/Admin/website/dist/download.html Mon Jul 04 14:42:06 2005 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,54 +0,0 @@
-<?xml version='1.0' encoding='iso-8859-1' ?>
-<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
-<!-- $Id$ -->
-<html xmlns="http://www.w3.org/1999/xhtml">
-
-<head>
- <title>Packages</title>
- <?include file="//include/htmlheader.include.html"?>
-</head>
-
-<body class="dist">
- <?include file="//include/header.include.html"?>
- <div class="hr"><hr/></div>
- <?include file="//include/navigation_dist.include.html"?>
- <div class="hr"><hr/></div>
-
- <div id="content">
- <?include file="//include/mirrorlist.minor.include.html"?>
- <div class="hr"><hr/></div>
-
- <h2><?value key="distname"?></h2>
-
- <p>The following source and binary packages of <?value key="distname"?>
- provide everything required for easy installation of the full Isabelle
- working environment on common Unix platforms (e.g. Linux, Darwin,
- Solaris). We provide a complete set of packages for Isabelle, Proof
- General, and PolyML.</p>
-
- <p>While XEmacs 21 is not included here, most operating system
- distributions already provide a suitable package. Some of the
- packages below are platform dependent; we include binaries for
- Linux/x86, Solaris/Sparc, and Darwin/PPC (MacOS X).</p>
-
- <p>Please see the <a href="installation.html">installation instructions</a>
- for which packages to download and for more information.</p>
-
- <?include file="//include/downloadtable.include.html"?>
-
- <h2>Development snapshot</h2>
-
- <p>For the curious we provide a nightly generated
- CVS <a href="http://isabelle.in.tum.de/devel/">development snapshot</a> of
- Isabelle. <em>Use at your own risk!</em></p>
-
- <h2>Past releases</h2>
-
- <p>Past releases are available from the <a href="download_past.html">archive</a>.</p>
-
- </div>
- <div class="hr"><hr/></div>
- <?include file="//include/footer.include.html"?>
-</body>
-
-</html>
--- a/Admin/website/dist/download_past.html Mon Jul 04 14:42:06 2005 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,46 +0,0 @@
-<?xml version='1.0' encoding='iso-8859-1' ?>
-<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
-<!-- $Id$ -->
-<html xmlns="http://www.w3.org/1999/xhtml">
-
-<head>
- <title>Older Isabelle Releases</title>
- <?include file="//include/htmlheader.include.html"?>
-</head>
-
-<body class="dist">
- <?include file="//include/header.include.html"?>
- <div class="hr"><hr/></div>
- <?include file="//include/navigation_dist.include.html"?>
- <div class="hr"><hr/></div>
-
- <div id="content">
- <?include file="//include/mirrorlist.minor.include.html"?>
- <div class="hr"><hr/></div>
-
- <h2>Archive</h2>
-
- Past releases of Isabelle are available from the Cambridge
- archive:
-
-<ul>
-<li><a href="http://www.cl.cam.ac.uk/users/lcp/archive/Isabelle2003.tar.gz">Isabelle2003</a></li>
-<li><a href="http://www.cl.cam.ac.uk/users/lcp/archive/Isabelle2002.tar.gz">Isabelle2002</a></li>
-<li><a href="http://www.cl.cam.ac.uk/users/lcp/archive/Isabelle99-2.tar.gz">Isabelle99-2</a></li>
-<li><a href="http://www.cl.cam.ac.uk/users/lcp/archive/Isabelle99-1.tar.gz">Isabelle99-1</a></li>
-<li><a href="http://www.cl.cam.ac.uk/users/lcp/archive/Isabelle99.tar.gz">Isabelle99</a></li>
-<li><a href="http://www.cl.cam.ac.uk/users/lcp/archive/Isabelle98-1.tar.gz">Isabelle98-1</a></li>
-<li><a href="http://www.cl.cam.ac.uk/users/lcp/archive/Isabelle98.tar.gz">Isabelle98</a></li>
-<li><a href="http://www.cl.cam.ac.uk/users/lcp/archive/Isabelle94-8.tar.gz">Isabelle94-8</a></li>
-<li><a href="http://www.cl.cam.ac.uk/users/lcp/archive/Isabelle94-7.tar.gz">Isabelle94-7</a></li>
-<li><a href="http://www.cl.cam.ac.uk/users/lcp/archive/Isabelle94-6.tar.gz">Isabelle94-6</a></li>
-<li><a href="http://www.cl.cam.ac.uk/users/lcp/archive/Isabelle94.tar.gz">Isabelle94</a></li>
-<li><a href="http://www.cl.cam.ac.uk/users/lcp/archive/Isabelle93.tar.gz">Isabelle93</a></li>
-</ul>
-
- </div>
- <div class="hr"><hr/></div>
- <?include file="//include/footer.include.html"?>
-</body>
-
-</html>
--- a/Admin/website/dist/index.html Mon Jul 04 14:42:06 2005 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,40 +0,0 @@
-<?xml version='1.0' encoding='iso-8859-1' ?>
-<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
-<!-- $Id$ -->
-<html xmlns="http://www.w3.org/1999/xhtml">
-
-<head>
- <title>Isabelle download mirrors</title>
- <?include file="//include/htmlheader.include.html"?>
-</head>
-
-<body class="dist">
- <?include file="//include/header.include.html"?>
- <div class="hr"><hr/></div>
- <?include file="//include/navigation_dist.include.html"?>
- <div class="hr"><hr/></div>
-
- <div id="content">
- <?include file="//include/mirrorlist.minor.include.html"?>
- <div class="hr"><hr/></div>
-
- <h2>Welcome to the Isabelle Distribution!</h2>
-
- <p>First, you might like to switch to a nearby mirror:</p>
-
- <ul>
- <li><a href="http://www.cl.cam.ac.uk/Research/HVG/Isabelle/dist/">Cambridge
- (UK)</a></li>
-
- <li><a href="http://isabelle.in.tum.de/dist/">Munich
- (Germany)</a></li>
-
- <li><a href="http://mirror.cse.unsw.edu.au/pub/isabelle/">Sydney
- (Australia)</a></li>
- </ul>
- </div>
- <div class="hr"><hr/></div>
- <?include file="//include/footer.include.html"?>
-</body>
-
-</html>
--- a/Admin/website/dist/installation.html Mon Jul 04 14:42:06 2005 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,203 +0,0 @@
-<?xml version='1.0' encoding='iso-8859-1' ?>
-<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
-<!-- $Id$ -->
-<html xmlns="http://www.w3.org/1999/xhtml">
-
-<head>
- <title>Installation instructions</title>
- <?include file="//include/htmlheader.include.html"?>
-</head>
-
-<body class="dist">
- <?include file="//include/header.include.html"?>
- <div class="hr"><hr/></div>
- <?include file="//include/navigation_dist.include.html"?>
- <div class="hr"><hr/></div>
-
- <div id="content">
- <?include file="//include/mirrorlist.minor.include.html"?>
- <div class="hr"><hr/></div>
-
- <h2>General</h2>
-
- <p>
- Isabelle runs on common Unix platforms.
- For Linux, Solaris and MaxOS / Darwin, we provide ready-to-install bundles;
- for other Unices, Isabelle has to be built from scratch.
- </p>
-
- <p>
- A usable Isabelle system consists of the following components:
- </p>
-
- <ul>
- <li>a suitable ML environment for Standard ML</li>
- <li>the Isabelle system itself, including the desired object logic(s)
- (e. g. HOL)</li>
- <li>the ProofGeneral user interface</li>
- </ul>
-
- <p>Optionally, theory graph browsing may be used if a Java JRE 1.1 or above
- is installed.</p>
-
- <p>For operating-system-specific instructions:</p>
-
- <ul>
- <li><a href="#install_linux">Linux (x86)</a></li>
- <li><a href="#install_solaris">Solaris (sparc)</a></li>
- <li><a href="#install_darwin">MacOS X / Darwin</a></li>
- <li><a href="#install_windows">Windows</a></li>
- </ul>
-
- <h2 id="install_linux">Linux</h2>
-
- <p>Commonly, an installation of Isabelle could work as follows:</p>
-
- <ul>
- <li>Ensure that your system has a running XEmacs 21 or Emacs 21
- with mule support (for ProofGeneral)</li>
- <li>Get the packages for <a href="http://www.polyml.org">Poly/ML</a>,
- <a href="http://proofgeneral.inf.ed.ac.uk/">ProofGeneral</a> (including
- the Emacs <a href="http://x-symbol.sourceforge.net">X-Symbol</a> package)
- and Isabelle,
- either from our <a href="download.html">package page</a> or from the
- links below. When you download ProofGeneral, please
- <a href="http://proofgeneral.inf.ed.ac.uk/register">register</a></li>
- <li>Likewise download the compiled image(s) of your desired object logic(s)</li>
- <li>Unpack the archives to an appropriate location, e. g.
- <tt class="shellcmd">/usr/local</tt>:
- <ul class="shellcmd">
- <li>tar -C /usr/local -xzf <?downloadLink target="//dist/packages/Isabelle2004.tar.gz"?></li>
- <li>tar -C /usr/local -xzf <?downloadLink target="//dist/packages/contrib/ProofGeneral.tar.gz"?></li>
- <li>tar -C /usr/local -xzf <?downloadLink target="//dist/packages/contrib/polyml_base.tar.gz"?></li>
- <li>tar -C /usr/local -xzf <?downloadLink target="//dist/packages/contrib/polyml_x86-linux.tar.gz"?></li>
- <li>tar -C /usr/local -xzf <?downloadLink target="//dist/packages/HOL_x86-linux.tar.gz"?></li>
- </ul>
- </li>
- <li>Under most circumstances, the default settings of Isabelle should be reasonable for
- invoking Isabelle/ProofGeneral without further ado:
- <ul class="shellcmd">
- <li>/usr/local/Isabelle/bin/Isabelle</li>
- </ul>
- Note that there is a separate option in
- the Proof General <em>Options</em> menu to enable X-Symbol.
- </li>
- <li>If Emacs appears to hang when the prover process is started, see the
- <a href="http://proofgeneral.inf.ed.ac.uk/FAQ">ProofGeneral FAQ</a> for
- advice.
- </li>
- </ul>
-
- <p>For more information, see the file <a href="//dist/packages/Isabelle/INSTALL">INSTALL</a>.</p>
-
- <h2 id="install_solaris">Solaris</h2>
-
- <p>Before you start, ensure the following for your system:</p>
- <ul>
- <li>GNU bash 2.x</li>
- <li>perl 5.x</li>
- <li>GNU tar 1.13 or higher</li>
- <li>GNU gzip 1.3 or higher</li>
- <li>running XEmacs 21 or Emacs 21
- with mule support (for ProofGeneral)</li>
- </ul>
-
- <p>Then, an installation on Solaris is analogous to Linux:</p>
-
- <ul>
- <li>Get the packages for <a href="http://www.polyml.org">Poly/ML</a>,
- <a href="http://proofgeneral.inf.ed.ac.uk/">ProofGeneral</a> (including
- the Emacs <a href="http://x-symbol.sourceforge.net">X-Symbol</a> package)
- and Isabelle,
- either from our <a href="download.html">package page</a> or from the
- links below. When you download ProofGeneral, please
- <a href="http://proofgeneral.inf.ed.ac.uk/register">register</a></li>
- <li>Likewise download the compiled image(s) of your desired object logic(s)</li>
- <li>Unpack the archives to an appropriate location, e. g.
- <tt class="shellcmd">/usr/local</tt>:
- <ul class="shellcmd">
- <li>gtar -C /usr/local -xzf <?downloadLink target="//dist/packages/Isabelle2004.tar.gz"?></li>
- <li>gtar -C /usr/local -xzf <?downloadLink target="//dist/packages/contrib/ProofGeneral.tar.gz"?></li>
- <li>gtar -C /usr/local -xzf <?downloadLink target="//dist/packages/contrib/polyml_base.tar.gz"?></li>
- <li>gtar -C /usr/local -xzf <?downloadLink target="//dist/packages/contrib/polyml_sparc-solaris.tar.gz"?></li>
- <li>gtar -C /usr/local -xzf <?downloadLink target="//dist/packages/HOL_sparc-solaris.tar.gz"?></li>
- </ul>
- </li>
- <li>Under most circumstances, the default settings of Isabelle should be reasonable for
- invoking Isabelle/ProofGeneral without further ado:
- <ul class="shellcmd">
- <li>/usr/local/Isabelle/bin/Isabelle</li>
- </ul>
- Note that there is a separate option in
- the Proof General <em>Options</em> menu to enable X-Symbol.
- </li>
- <li>If Emacs appears to hang when the prover process is started, see the
- <a href="http://proofgeneral.inf.ed.ac.uk/FAQ">ProofGeneral FAQ</a> for
- advice.
- </li>
- </ul>
-
- <p>For more information, see the file <a href="//dist/packages/Isabelle/INSTALL">INSTALL</a>.</p>
-
- <h2 id="install_darwin">MaxOS X / Darwin</h2>
-
- <p>Before you start, ensure the following for your system:</p>
- <ul>
- <li>running MacOS X 10.2.2 or higher</li>
- <li>running XEmacs 21 or Emacs 21 with mule support (for ProofGeneral)
- – for further reference, see the
- <a href="installation_macos_emacs.html">MacOS X Emacs hints</a>
- </li>
- </ul>
-
- <p>Then, an installation on Darwin is analogous to Linux:</p>
-
- <ul>
- <li>Get the packages for <a href="http://www.polyml.org">Poly/ML</a>,
- <a href="http://proofgeneral.inf.ed.ac.uk/">ProofGeneral</a> (including
- the Emacs <a href="http://x-symbol.sourceforge.net">X-Symbol</a> package)
- and Isabelle,
- either from our <a href="download.html">package page</a> or from the
- links below. When you download ProofGeneral, please
- <a href="http://proofgeneral.inf.ed.ac.uk/register">register</a></li>
- <li>Likewise download the compiled image(s) of your desired object logic(s)</li>
- <li>Unpack the archives to an appropriate location, e. g.
- <tt class="shellcmd">/usr/local</tt>:
- <ul class="shellcmd">
- <li>gtar -C /usr/local -xzf <?downloadLink target="//dist/packages/Isabelle2004.tar.gz"?></li>
- <li>gtar -C /usr/local -xzf <?downloadLink target="//dist/packages/contrib/ProofGeneral.tar.gz"?></li>
- <li>gtar -C /usr/local -xzf <?downloadLink target="//dist/packages/contrib/polyml_base.tar.gz"?></li>
- <li>gtar -C /usr/local -xzf <?downloadLink target="//dist/packages/contrib/polyml_ppc-darwin.tar.gz"?></li>
- <li>gtar -C /usr/local -xzf <?downloadLink target="//dist/packages/HOL_ppc-darwin.tar.gz"?></li>
- </ul>
- </li>
- <li>Under most circumstances, the default settings of Isabelle should be reasonable for
- invoking Isabelle/ProofGeneral without further ado:
- <ul class="shellcmd">
- <li>/usr/local/Isabelle/bin/Isabelle</li>
- </ul>
- Note that there is a separate option in
- the Proof General <em>Options</em> menu to enable X-Symbol.
- </li>
- <li>If Emacs appears to hang when the prover process is started, see the
- <a href="http://proofgeneral.inf.ed.ac.uk/FAQ">ProofGeneral FAQ</a> for
- advice.
- </li>
- </ul>
-
- <h2 id="install_windows">Windows</h2>
-
- <p>Isabelle does not run nativly on Windows; in a restricted fashion,
- you may run Isabelle on Windows using the Cygwin environment.
- See <a href="installation_notes_cygwin.html">Installation notes for
- Cygwin/Windows</a>.</p>
-
- <p>For a serious apporach, you should consider a Windows/Linux dualboot
- installation.</p>
-
- </div>
- <div class="hr"><hr/></div>
- <?include file="../include/footer.include.html"?>
-</body>
-
-</html>
--- a/Admin/website/dist/installation_macos_emacs.html Mon Jul 04 14:42:06 2005 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,76 +0,0 @@
-<?xml version='1.0' encoding='iso-8859-1' ?>
-<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
-<!-- $Id$ -->
-<html xmlns="http://www.w3.org/1999/xhtml">
-
-<head>
- <title>MacOS X Emacs hints</title>
- <?include file="//include/htmlheader.include.html"?>
-</head>
-
-<body class="dist">
- <?include file="//include/header.include.html"?>
- <div class="hr"><hr/></div>
- <?include file="//include/navigation_dist.include.html"?>
- <div class="hr"><hr/></div>
- <div id="content">
-
- <h2>MacOS X Emacs hints</h2>
-
- <p>Assuming you have an installation of Isabelle on your Mac,
- there are various possibilites for running ProofGeneral:</p>
-
- <ul>
- <li>You should also be able to launch <a href=
- "http://proofgeneral.inf.ed.ac.uk/">Proof General</a> by typing
- <tt class="shellcmd">Isabelle</tt> at the Unix command line. This will invoke the
- Apple-supplied version of Emacs in a terminal window, providing a primitive
- environment.</li>
- <li>Somewhat better is to run Proof General from within a version
- of Emacs ported as a native Mac OS X application, such as <a href=
- "http://home.att.ne.jp/alpha/z123/emacs-mac-e.html">MacEmacs JP</a> or
- <a href="http://mindlube.com/products/emacs/">mindlube's</a> or <a href=
- "http://www.cs.man.ac.uk/%7efranconi/mac-emacs/">Enhanced Carbon Emacs</a>.
- Visiting a theory file from Emacs will automatically launch Proof General
- provided <tt class="shellcmd">isabelle</tt> is on the search path. None of these options
- support the X-Symbol package, unfortunately.</li>
- <li>In order to get the full benefit of Proof General, you must install the X
- Window System (X11) and <a href="http://www.xemacs.org/">XEmacs</a> or
- <a href="http://www.gnu.org/software/emacs/emacs.html">GNU Emacs</a>.</li>
- <ul>
- <li>
- <a href="http://www.apple.com/macosx/x11/">apple's version of X11</a>
- is included with the Panther (MacOS X 10.3) installation discs, though it is
- not installed by default. The Command key serves as Meta, but it is
- reserved for standard Apple shortcuts such as C, V and X, so you must use
- Esc-C, Esc-V and Esc-X in Emacs or else deselect »Enable key equivalents«
- in the X11 preferences.</li>
- <li>The easiest way to install XEmacs or GNU Emacs is via the package manager
- <a href="http://fink.sourceforge.net/">Fink</a>. Install the Fink package
- <tt>xemacs-sumo-pkg</tt> to get the XEmacs libraries that Proof General needs
- to run. To install GNU Emacs, install the package <tt>emacs21</tt>. Fink can
- compile from sources, but this takes hours, so it is better to request binary
- installations.</li>
- <li>To use <a href="http://www.gnu.org/software/emacs/emacs.html">GNU
- Emacs</a> instead of <a href="http://www.xemacs.org/">XEmacs</a>, you must
- recompile Proof General and X-Symbol following the instructions <a href=
- "http://proofgeneral.inf.ed.ac.uk/FAQ">here</a>. Note that Proof General
- incorporates its own copy of X-Symbol.</li>
-
- </ul>
- </ul>
-
- <p>You may want to install this drag-and-drop <a href=
- "//dist/misc/isabelle_droplet.dmg">Isabelle launcher</a>. It is a simple hack that
- invokes XEmacs on any files dropped on it.</p>
-
- <p>Here is a <a href=
- "//dist/img/screenshot_isabelle_macos.gif">screenshot</a> showing Proof General running
- in GNU Emacs.</p>
-
- </div>
- <div class="hr"><hr/></div>
- <?include file="../include/footer.include.html"?>
-</body>
-
-</html>
--- a/Admin/website/dist/installation_notes_cygwin.html Mon Jul 04 14:42:06 2005 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,267 +0,0 @@
-<?xml version='1.0' encoding='iso-8859-1' ?>
-<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
-<!-- $Id$ -->
-<html xmlns="http://www.w3.org/1999/xhtml">
-
-<head>
- <title>Installation notes for Windows/Cygwin</title>
- <?include file="//include/htmlheader.include.html"?>
-</head>
-
-<body class="dist">
- <?include file="//include/header.include.html"?>
- <div class="hr"><hr/></div>
- <?include file="//include/navigation_dist.include.html"?>
- <div class="hr"><hr/></div>
-
- <div id="content">
- <?include file="//include/mirrorlist.minor.include.html"?>
- <div class="hr"><hr/></div>
-
- <h2>Preconditions and restrictions</h2>
-
- <p>Please notice before you go ahead:</p>
-
- <ul>
- <li>The ML system these notes apply to is <a href=
- "http://www.smlnj.org/">Standard ML of New Jersey</a>; it is <em>not</em>
- known yet how to get Isabelle run completely with <a href=
- "www.polyml.org/">Poly/ML</a>. See <a href="#polyml">a note on Poly/ML</a>
- down this page.</li>
-
- <li>It is assumed you have some experience with an Unix operating system
- (e.g. what a shell is for and how to use it).</li>
- </ul>
-
- <p>Any suggestions and improvements concerning this hints are welcomed!</p>
-
- <h2>Acknowlegements</h2>
-
- <p>Thanks to <a href=
- "http://cswww.essex.ac.uk/Research/FSS/projects/isawin/">Norbert
- Völker</a> and <a href=
- "http://www.abo.fi/~viorel.preoteasa/isabelle/">Viorel Preoteasa</a> whose
- efforts helped a lot to get Isabelle run this way.</p>
-
- <h2>Installing Cygwin</h2>
-
- <p>Cygwin is a POSIX emulation layer for Windows; it contains ports of a
- large collection of common Unix software (shells, perl, gcc, X11, latex,
- ImageMagick, …).</p>
-
- <p>To install it, get the installer from the <a href=
- "http://www.cygwin.com">Cygwin website</a> and run it. It will ask you which
- packages to install, and then downloads and installs them. Please make sure
- you install everything needed by Isabelle; it is hard to give a concise list
- of packages here since the bundling of Cygwin packages may vary over time,
- but installing the base packages, perl, make, xemacs and x-server should be a
- good choice for the beginning.</p>
-
- <p>By default, cygwin installs to <tt class="shellcmd">c:\cygwin</tt>; you may choose an
- arbitrary location, but it is recommended that it does not include any space
- or exotic characters. This directory will then become the root directory of
- the Cygwin filesystem tree, i.e. the Cygwin path <tt class="shellcmd">/opt/smlnj</tt> will be
- mapped to Windows path <tt class="shellcmd">c:\cygwin\opt\smlnj</tt>.</p>
-
- <p>After installation, open a Cygwin shell window (normally the installer
- makes a shortcut for you).</p>
-
- <h2>Getting and building SML/NJ</h2>
-
- <p>Now we are ready to get and build <a href=
- "http://www.smlnj.org/">SML/NJ</a>; before this, set the environment variable
- SMLNJ_CYGWIN_RUNTIME to 1:</p>
-
- <ul class="shellcmd">
- <li>export SMLNJ_CYGWIN_RUNTIME=1</li>
- </ul>
-
- <p>This setting will tell the build process that it should
- <em>not</em> attempt to build SML/NJ natively for Win32 but for Cygwin
- instead (see further <a href=
- "http://smlnj.cs.uchicago.edu/dist/working/110.53/CYGWININSTALL">CYGWININSTALL</a>).</p>
-
- <p>So far, this setup was tested using the working version 110.53 of SML/NJ
- from <a href=
- "http://smlnj.cs.uchicago.edu/dist/working/110.53/">http://smlnj.cs.uchicago.edu/dist/working/110.53/</a>.
- SML/NJ provides a nice installer enabling you to download and build it. Read
- <a href=
- "http://smlnj.cs.uchicago.edu/dist/working/110.53/INSTALL">INSTALL</a> to
- learn about the different possibilites to do this. The default packages
- should be sufficient.</p>
-
- <p>In the following, it is assumed that you install SML/NJ to Cygwin path
- <tt class="shellcmd">/opt/smlnj</tt>; if you choose an other location, some tweaking in the
- <a href="#config"><tt class="shellcmd">etc/settings</tt> file</a> may be neccessary later.</p>
-
- <p>Whenever SMLNJ is used, the SMLNJ_CYGWIN_RUNTIME environment variable must
- be set to 1 (later on a convenient mechanism to make this the default is
- proposed).</p>
-
- <h2>Installing Isabelle</h2>
-
- <p>Download the latest Isabelle and ProofGeneral <a href=
- "download.html">release packages</a>. Assuming that you are in the directory
- where you downloaded the files, install them into <tt class="shellcmd">/opt</tt> by typing
- into the bash shell:</p>
-
- <ul class="shellcmd">
- <li>tar -C /usr/opt -xvzf <?value key="distname"?>.tar.gz</li>
- <li>tar -C /usr/opt -xvzf ProofGeneral.tar.gz</li>
- </ul>
-
- <p>During extraction, one inconvenience may occur, see <a href=
- "#inconvenience">below</a>.</p>
-
- <p>The location <tt class="shellcmd">/opt</tt> again is just a proposal; if you choose other
- locations, some tweaking in the <a href="#config"><tt class="shellcmd">etc/settings</tt>
- file</a> may be neccessary later.</p>
-
- <h2 id="config">Configuring Isabelle</h2>
-
- <p>Edit the file <tt class="shellcmd">/opt/Isabelle/etc/settings</tt>; first, uncomment the
- lines about SMLNJ. Also set the variable SMLNJ_CYGWIN_RUNTIME to 1, in order
- the cygwin version of SMLNJ is used. As mentioned above, the path variables
- for the ML system and ProofGeneral may need adjustions, depending on your
- different installation locations.</p>
-
- <p>Take heed of the setting of ISABELLE_HOME_USER; by default, this is
- <tt class="shellcmd">~/isabelle</tt>. To detect which Windows path this will be mapped to,
- type into the Cygwin bash shell:</p>
-
- <ul class="shellcmd">
- <li>cygpath --windows ~/isabelle</li>
- </ul>
-
- <p>If you don't like this location to be the isabelle home
- directory, consider setting of ISABELLE_HOME_USER to another value; use
- <tt class="shellcmd">cygpath --unix <winpath></tt> to detect which Cygwin path a given
- Windows path is mapped to.</p>
-
- <p>A typical change could look like this:</p>
-
- <blockquote>
- from<br />
- <tt># Standard ML of New Jersey 110 or later<br />
- #ML_SYSTEM=smlnj-110<br />
- #ML_HOME="$ISABELLE_HOME/../smlnj/bin"<br />
- #ML_OPTIONS="@SMLdebug=/dev/null"<br />
- #ML_PLATFORM=$(eval $("$ML_HOME/.arch-n-opsys" 2>/dev/null); echo
- "$HEAP_SUFFIX")<br /></tt>
- </blockquote>
-
- <blockquote>
- to<br />
- <tt># Standard ML of New Jersey 110 or later<br />
- SMLNJ_CYGWIN_RUNTIME=1<br />
- ML_SYSTEM=smlnj-110<br />
- ML_HOME="$ISABELLE_HOME/../smlnj/bin"<br />
- ML_OPTIONS="@SMLdebug=/dev/null"<br />
- ML_PLATFORM=$(eval $("$ML_HOME/.arch-n-opsys" 2>/dev/null); echo
- "$HEAP_SUFFIX")</tt>
- </blockquote>
-
- <h2>Building logics</h2>
-
- <p>Now we can compile some logics. Start the cygwin shell (if not still
- running) and type:</p>
-
- <ul class="shellcmd">
- <li>cd /opt/Isabelle</li>
- <li>build HOL</li>
- <li>build ZF</li>
- </ul>
-
- <p>The compilation process may take some time (depending on how fast the
- computer is). Before building a logic image the build program shows some
- variables and expects user input – just hit enter.</p>
-
- <h2>Running Isabelle with ProofGeneral</h2>
-
- <p>On Linux, Isabelle can be started by two scripts located in
- <tt class="shellcmd">Isabelle/bin</tt>: <tt class="shellcmd">Isabelle</tt> and <tt class="shellcmd">isabelle</tt>.
- <tt class="shellcmd">Isabelle</tt> attempts to start ProofGeneral with XEmacs, and isabelle
- starts it in an SML shell session. However Windows treats the two names as
- one. To get around this, just rename <tt class="shellcmd">/opt/Isabelle/bin/isabelle</tt> to
- <tt class="shellcmd">/opt/Isabelle/bin/Isabelle</tt>. This script
- will start Isabelle with ProofGeneral; the <tt class="shellcmd">isabelle</tt>
- script in any case is available as <tt class="shellcmd">isabelle-process</tt>.</p>
-
- <p>Now everything should be ready. To test, start the cygwin shell and
- type</p>
-
- <ul class="shellcmd">
- <li>startx &</li>
- </ul>
-
- <p>This will start the cygwin X server and an X shell window. In
- the X shell window, type</p>
-
- <ul class="shellcmd">
- <li>/opt/Isabelle/bin/Isabelle &</li>.
- </ul>
-
- <p>This will start the ProofGeneral interface for Isabelle. After a
- while an empty buffer <tt>Scratch.thy</tt> is created. You can turn on
- X-Symbol from the menu Proof-General, item Options.</p>
-
- <p>Load one of your favorite theories and test your Isabelle installation by
- proving something.</p>
-
- <p>To simplify starting ProofGeneral, consider writing a Windows command
- script, e. g.</p>
-
- <blockquote>
- <tt>@bash startx -geometry 30x4 -iconic -e Isabell</tt>
- </blockquote>
-
- <p>and assigning a shortcut in the start menu to it.</p>
-
- <h2 id="inconvenience">Inconveniencies with the current version of
- Isabelle</h2>
-
- <p>With the current Isabelle release (Isabelle 2004), there are two
- inconveniencies:</p>
-
- <ul>
- <li>During extraction you will get a warning that file
- <tt class="shellcmd">Real/HahnBanach/Aux.thy</tt> can not be created. This is because
- <tt class="shellcmd">Aux</tt> is not allowed as a filename under Windows. If you do not want
- to run the HahnBanach example, you might simply want to ignore this
- warning.</li>
-
- <li>The tool <tt class="shellcmd">isatool mkdir</tt> tries to detect the name of the current
- user, to put it into the generated <tt class="shellcmd">root.tex</tt>. Alas, on Windows,
- this leads to an unquoted <tt>\</tt> in the TeX file. So you either must
- edit your <tt class="shellcmd">root.tex</tt> manually to fix this, or directly patch
- <tt class="shellcmd">/opt/Isabelle/lib/Tools/mkdir</tt> by replacing
-
- <blockquote>
- <tt>AUTHOR=$("$AUTO_PERL" -e "@pw = getpwnam(\"$USER\"); print @pw[6]" | tr _ -)</tt>
- </blockquote>with
-
- <blockquote>
- <tt>AUTHOR="default author name"</tt>
- </blockquote>
- </li>
- </ul>
-
- <p>To get around these inconveniencies, consider using a recent developer
- snapshot of Isabelle; both will be fixed in the next Isabelle release.</p>
-
- <h2 id="polyml">A note on Poly/ML</h2>
-
- <p>As indicated above, Isabelle does <em>not</em> run neatly with <a href=
- "http://www.polyml.org/">Poly/ML</a> on Windows, since it is not clear
- how Poly/ML has to be compiled for Cygwin, and the native Windows port
- of PolyML does not provide some Posix signals Isabelle/ProofGeneral relies on.</p>
-
- <p>If you know how to circumvent (fully or partially) any of these problems,
- please let us know.</p>
-
- </div>
- <div class="hr"><hr/></div>
- <?include file="../include/footer.include.html"?>
-</body>
-
-</html>
--- a/Admin/website/dist/installation_notes_macosx.html Mon Jul 04 14:42:06 2005 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,120 +0,0 @@
-<?xml version='1.0' encoding='iso-8859-1' ?>
-<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
-<!-- $Id$ -->
-<html xmlns="http://www.w3.org/1999/xhtml">
-
-<head>
- <title>Installation hints for Mac OS X</title>
- <?include file="//include/htmlheader.include.html"?>
-</head>
-
-<body class="dist">
- <?include file="//include/header.include.html"?>
- <div class="hr"><hr/></div>
- <?include file="//include/navigation_dist.include.html"?>
- <div class="hr"><hr/></div>
- <div id="content">
-
- <h2>Installing on Mac OS X</h2>
- <p><a href="http://www.apple.com/macosx/">Mac OS X</a> is the current version
- of the Macintosh operating system, installed on all new <a href=
- "http://www.apple.com/">Apple</a> computers. Because it is based on Unix, it
- can run <a href=
- "http://www.cl.cam.ac.uk/Research/HVG/Isabelle/">Isabelle</a>. The new
- <a href="http://www.apple.com/powermac/">Power Mac G5</a> is an excellent
- Isabelle machine. Here is a <a href=
- "//dist/img/screenshot_isabelle_macos.gif">screenshot</a> showing Proof General running
- in GNU Emacs.</p>
-
- <p>This page gives advice on building Isabelle for Mac OS X. It assumes that
- you are familiar with both Mac OS X and Unix. You must have installed the Mac
- OS X developer tools.</p>
-
- <ol>
- <li>Download Isabelle to a suitable directory, as described on the
- <a href="download.html">download page</a>. Be sure to get the following
- files
-
- <ul>
- <li><?value key="distname"?>.tar.gz</li>
- <li>ProofGeneral.tar.gz</li>
- <li>polyml_base.tar.gz</li>
- <li>polyml_ppc-darwin.tar.gz</li>
- <li>HOL_ppc-darwin.tar.gz</li>
- </ul>
- </li>
-
- <li>You may have to install the bash shell. Versions of Mac OS X prior to
- 10.2.2 did not provide it. If /bin/bash does not exist, you can install it
- using the package manager <a href=
- "http://fink.sourceforge.net/">Fink</a>.</li>
-
- <li>At this point, you should be able to run Isabelle with the command line
- interface. You can also build Isabelle from the Unix command line,
- following the instructions for "Compiling Logics" in file
- <tt class="shellcmd">Isabelle/INSTALL.</tt></li>
-
- <li>You should also be able to launch <a href=
- "http://proofgeneral.inf.ed.ac.uk/">Proof General</a> by typing
- <tt class="shellcmd">Isabelle</tt> at the Unix command line. This will invoke the
- Apple-supplied version of Emacs in a terminal window, providing a primitive
- environment. Somewhat better is to run Proof General from within a version
- of Emacs ported as a native Mac OS X application, such as <a href=
- "http://home.att.ne.jp/alpha/z123/emacs-mac-e.html">MacEmacs JP</a> or
- <a href="http://mindlube.com/products/emacs/">mindlube's</a> or <a href=
- "http://www.cs.man.ac.uk/%7efranconi/mac-emacs/">Enhanced Carbon Emacs</a>.
- Visiting a theory file from Emacs will automatically launch Proof General
- provided <tt class="shellcmd">isabelle</tt> is on the search path. None of these options
- support the X-Symbol package, unfortunately.</li>
- </ol>
-
- <p>In order to get the full benefit of Proof General, you must install the X
- Window System (X11) and <a href="http://www.xemacs.org/">XEmacs</a> or
- <a href="http://www.gnu.org/software/emacs/emacs.html">GNU Emacs</a>.</p>
-
- <ul>
- <li><a href="http://www.apple.com/macosx/x11/">Apple's version</a> of X11
- is included with the Panther (MacOS 10.3) installation discs, though it is
- not installed by default. The Command key serves as Meta, but it is
- reserved for standard Apple shortcuts such as C, V and X, so you must use
- Esc-C, Esc-V and Esc-X in Emacs or else deselect "Enable key equivalents"
- in the X11 preferences.</li>
-
- <li>Some people prefer the <a href=
- "http://www.osxgnu.org/software/Xwin/WindowManagers/OroborOSX/">OroborOSX</a>
- window manager. It must be used in conjunction with <a href=
- "http://xfree86.org/">XFree86</a>, which is easy to install if you use the
- installer provided by the <a href=
- "http://sourceforge.net/projects/xonx/">XonX</a> project.</li>
- </ul>
-
- <p>The easiest way to install XEmacs or GNU Emacs is via the package manager
- <a href="http://fink.sourceforge.net/">Fink</a>. Install the Fink package
- <tt>xemacs-sumo-pkg</tt> to get the XEmacs libraries that Proof General needs
- to run. To install GNU Emacs, install the package <tt>emacs21</tt>. Fink can
- compile from sources, but this takes hours, so it is better to request binary
- installations.</p>
-
- <p>To use <a href="http://www.gnu.org/software/emacs/emacs.html">GNU
- Emacs</a> instead of <a href="http://www.xemacs.org/">XEmacs</a>, you must
- recompile Proof General and X-Symbol following the instructions <a href=
- "http://proofgeneral.inf.ed.ac.uk/FAQ">here</a>. Note that Proof General
- incorporates its own copy of X-Symbol.</p>
-
- <ol>
- <li>Install X11 or OroborOSX.</li>
-
- <li>Install XEmacs (and its libraries), or install GNU Emacs and recompile
- Proof General.</li>
-
- <li>You may want to install this drag-and-drop <a href=
- "IsabelleDroplet.dmg">Isabelle launcher</a>. It is a simple hack that
- invokes xemacs on any files dropped on it.</li>
- </ol>
-
- </div>
- <div class="hr"><hr/></div>
- <?include file="../include/footer.include.html"?>
-</body>
-
-</html>
--- a/Admin/website/dist/others.html Mon Jul 04 14:42:06 2005 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,35 +0,0 @@
-<?xml version='1.0' encoding='iso-8859-1' ?>
-<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
-<!-- $Id$ -->
-<html xmlns="http://www.w3.org/1999/xhtml">
-
-<head>
- <title>Other Isabelle resources</title>
- <?include file="//include/htmlheader.include.html"?>
-</head>
-
-<body class="dist">
- <?include file="//include/header.include.html"?>
- <div class="hr"><hr/></div>
- <?include file="//include/navigation_dist.include.html"?>
- <div class="hr"><hr/></div>
- <div id="content">
- <h2>More about Isabelle</h2>
-
- <p>is available on our main sites:</p>
-
- <ul>
- <li>at <a href=
- "http://www.cl.cam.ac.uk/Research/HVG/Isabelle/index.html">Cambridge
- (UK)</a></li>
-
- <li>at <a href="http://isabelle.in.tum.de/index.html">Munich
- (Germany)</a></li>
- </ul>
-
- </div>
- <div class="hr"><hr/></div>
- <?include file="//include/footer.include.html"?>
-</body>
-
-</html>
--- a/Admin/website/documentation.html Mon Jul 04 14:42:06 2005 +0200
+++ b/Admin/website/documentation.html Mon Jul 04 15:15:55 2005 +0200
@@ -8,15 +8,14 @@
<?include file="//include/htmlheader.include.html"?>
</head>
-<body class="dist">
+<body>
<?include file="//include/header.include.html"?>
<div class="hr"><hr/></div>
<?include file="//include/navigation.include.html"?>
<div class="hr"><hr/></div>
<div id="content">
- <?include file="//include/mirrorlist.include.html"?>
- <div class="hr"><hr/></div>
+
<h2>Getting started</h2>
<a href="//dist/img/tutorial_cover_big.gif">
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/website/download_past.html Mon Jul 04 15:15:55 2005 +0200
@@ -0,0 +1,43 @@
+<?xml version='1.0' encoding='iso-8859-1' ?>
+<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
+<!-- $Id$ -->
+<html xmlns="http://www.w3.org/1999/xhtml">
+
+<head>
+ <title>Older Isabelle Releases</title>
+ <?include file="//include/htmlheader.include.html"?>
+</head>
+
+<body class="dist">
+ <?include file="//include/header.include.html"?>
+ <div class="hr"><hr/></div>
+ <?include file="//include/navigation.include.html"?>
+ <div class="hr"><hr/></div>
+
+ <div id="content">
+
+ <h2>Archive</h2>
+
+ Past releases of Isabelle are available from the Cambridge
+ archive:
+ <ul>
+ <li><a href="http://www.cl.cam.ac.uk/users/lcp/archive/Isabelle2003.tar.gz">Isabelle2003</a></li>
+ <li><a href="http://www.cl.cam.ac.uk/users/lcp/archive/Isabelle2002.tar.gz">Isabelle2002</a></li>
+ <li><a href="http://www.cl.cam.ac.uk/users/lcp/archive/Isabelle99-2.tar.gz">Isabelle99-2</a></li>
+ <li><a href="http://www.cl.cam.ac.uk/users/lcp/archive/Isabelle99-1.tar.gz">Isabelle99-1</a></li>
+ <li><a href="http://www.cl.cam.ac.uk/users/lcp/archive/Isabelle99.tar.gz">Isabelle99</a></li>
+ <li><a href="http://www.cl.cam.ac.uk/users/lcp/archive/Isabelle98-1.tar.gz">Isabelle98-1</a></li>
+ <li><a href="http://www.cl.cam.ac.uk/users/lcp/archive/Isabelle98.tar.gz">Isabelle98</a></li>
+ <li><a href="http://www.cl.cam.ac.uk/users/lcp/archive/Isabelle94-8.tar.gz">Isabelle94-8</a></li>
+ <li><a href="http://www.cl.cam.ac.uk/users/lcp/archive/Isabelle94-7.tar.gz">Isabelle94-7</a></li>
+ <li><a href="http://www.cl.cam.ac.uk/users/lcp/archive/Isabelle94-6.tar.gz">Isabelle94-6</a></li>
+ <li><a href="http://www.cl.cam.ac.uk/users/lcp/archive/Isabelle94.tar.gz">Isabelle94</a></li>
+ <li><a href="http://www.cl.cam.ac.uk/users/lcp/archive/Isabelle93.tar.gz">Isabelle93</a></li>
+ </ul>
+
+ </div>
+ <div class="hr"><hr/></div>
+ <?include file="//include/footer.include.html"?>
+</body>
+
+</html>
--- a/Admin/website/include/mirrorlist.include.html Mon Jul 04 14:42:06 2005 +0200
+++ b/Admin/website/include/mirrorlist.include.html Mon Jul 04 15:15:55 2005 +0200
@@ -2,9 +2,11 @@
<!DOCTYPE div PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
<!-- $Id$ -->
<div class="mirrorlist">
- <p>Switch mirror:</p>
+ <div class="hr"><hr/></div>
+ <h3>Site Mirrors:</h3>
<ul>
<li><?mirror prefix="http://www.cl.cam.ac.uk/Research/HVG/Isabelle/" title="Cambridge (.uk)" ?></li>
<li><?mirror prefix="http://isabelle.in.tum.de/" title="Munich (.de)" ?></li>
+ <li><?mirror prefix="http://mirror.cse.unsw.edu.au/pub/isabelle/" title="Sydney (.au)" ?></li>
</ul>
</div>
--- a/Admin/website/include/mirrorlist.major.include.html Mon Jul 04 14:42:06 2005 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,10 +0,0 @@
-<?xml version='1.0' encoding='iso-8859-1' ?>
-<!DOCTYPE div PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
-<!-- $Id$ -->
-<div class="mirrorlist">
- <p>Switch mirror:</p>
- <ul>
- <li><?mirror prefix="http://www.cl.cam.ac.uk/Research/HVG/Isabelle/" title="Cambridge (.uk)" ?></li>
- <li><?mirror prefix="http://isabelle.in.tum.de/" title="Munich (.de)" ?></li>
- </ul>
-</div>
--- a/Admin/website/include/mirrorlist.minor.include.html Mon Jul 04 14:42:06 2005 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,11 +0,0 @@
-<?xml version='1.0' encoding='iso-8859-1' ?>
-<!DOCTYPE div PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
-<!-- $Id$ -->
-<div class="mirrorlist">
- <p>Switch mirror:</p>
- <ul>
- <li><?mirror prefix="http://www.cl.cam.ac.uk/Research/HVG/Isabelle/" title="Cambridge (.uk)" ?></li>
- <li><?mirror prefix="http://isabelle.in.tum.de/" title="Munich (.de)" ?></li>
- <li><?mirror prefix="http://mirror.cse.unsw.edu.au/pub/isabelle/" title="Sydney (.au)" stripprefix="dist/" ?></li>
- </ul>
-</div>
--- a/Admin/website/include/navigation.include.html Mon Jul 04 14:42:06 2005 +0200
+++ b/Admin/website/include/navigation.include.html Mon Jul 04 15:15:55 2005 +0200
@@ -7,7 +7,10 @@
<?navitem target="index.html" title="Home" ?>
<?navitem target="overview.html" title="Overview" ?>
<?navitem target="logics.html" title="Logics" ?>
+ <?navitem target="installation.html" title="Installation" ?>
+ <?navitem target="packages.html" title="Packages" ?>
+ <?navitem target="documentation.html" title="Documentation" ?>
<?navitem target="community.html" title="Community" ?>
- <?navitem target="dist/index.html" title="Distribution" ?>
+ <li><?include file="//include/mirrorlist.include.html"?></li>
</ul>
</div>
--- a/Admin/website/include/navigation_dist.include.html Mon Jul 04 14:42:06 2005 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,13 +0,0 @@
-<?xml version='1.0' encoding='iso-8859-1' ?>
-<!DOCTYPE div PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
-<!-- $Id$ -->
-<div id="navigation">
- <h2>Navigation</h2>
- <ul>
- <?navitem target="index.html" title="Mirrors" ?>
- <?navitem target="installation.html" title="Installation" ?>
- <?navitem target="download.html" title="Packages" ?>
- <?navitem target="documentation.html" title="Documentation" ?>
- <?navitem target="others.html" title="Other links" ?>
- </ul>
-</div>
--- a/Admin/website/index.html Mon Jul 04 14:42:06 2005 +0200
+++ b/Admin/website/index.html Mon Jul 04 15:15:55 2005 +0200
@@ -101,7 +101,7 @@
<p>
The Isabelle distribution is distributed <em>for free</em> and available
-from several <a href="dist/index.html">mirror sites</a>. It includes
+from several <a href="mirrors.html">mirror sites</a>. It includes
source and binary packages and browsable documentation. You can also
browse the <a href="//library/index.html">Isabelle theory library</a>
online.
--- a/Admin/website/installation.html Mon Jul 04 14:42:06 2005 +0200
+++ b/Admin/website/installation.html Mon Jul 04 15:15:55 2005 +0200
@@ -8,15 +8,13 @@
<?include file="//include/htmlheader.include.html"?>
</head>
-<body class="dist">
+<body>
<?include file="//include/header.include.html"?>
<div class="hr"><hr/></div>
<?include file="//include/navigation.include.html"?>
<div class="hr"><hr/></div>
<div id="content">
- <?include file="//include/mirrorlist.include.html"?>
- <div class="hr"><hr/></div>
<h2>General</h2>
@@ -197,7 +195,7 @@
</div>
<div class="hr"><hr/></div>
- <?include file="../include/footer.include.html"?>
+ <?include file="//include/footer.include.html"?>
</body>
</html>
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/website/installation_macos_emacs.html Mon Jul 04 15:15:55 2005 +0200
@@ -0,0 +1,76 @@
+<?xml version='1.0' encoding='iso-8859-1' ?>
+<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
+<!-- $Id$ -->
+<html xmlns="http://www.w3.org/1999/xhtml">
+
+<head>
+ <title>MacOS X Emacs hints</title>
+ <?include file="//include/htmlheader.include.html"?>
+</head>
+
+<body class="dist">
+ <?include file="//include/header.include.html"?>
+ <div class="hr"><hr/></div>
+ <?include file="//include/navigation.include.html"?>
+ <div class="hr"><hr/></div>
+ <div id="content">
+
+ <h2>MacOS X Emacs hints</h2>
+
+ <p>Assuming you have an installation of Isabelle on your Mac,
+ there are various possibilites for running ProofGeneral:</p>
+
+ <ul>
+ <li>You should also be able to launch <a href=
+ "http://proofgeneral.inf.ed.ac.uk/">Proof General</a> by typing
+ <tt class="shellcmd">Isabelle</tt> at the Unix command line. This will invoke the
+ Apple-supplied version of Emacs in a terminal window, providing a primitive
+ environment.</li>
+ <li>Somewhat better is to run Proof General from within a version
+ of Emacs ported as a native Mac OS X application, such as <a href=
+ "http://home.att.ne.jp/alpha/z123/emacs-mac-e.html">MacEmacs JP</a> or
+ <a href="http://mindlube.com/products/emacs/">mindlube's</a> or <a href=
+ "http://www.cs.man.ac.uk/%7efranconi/mac-emacs/">Enhanced Carbon Emacs</a>.
+ Visiting a theory file from Emacs will automatically launch Proof General
+ provided <tt class="shellcmd">isabelle</tt> is on the search path. None of these options
+ support the X-Symbol package, unfortunately.</li>
+ <li>In order to get the full benefit of Proof General, you must install the X
+ Window System (X11) and <a href="http://www.xemacs.org/">XEmacs</a> or
+ <a href="http://www.gnu.org/software/emacs/emacs.html">GNU Emacs</a>.</li>
+ <ul>
+ <li>
+ <a href="http://www.apple.com/macosx/x11/">apple's version of X11</a>
+ is included with the Panther (MacOS X 10.3) installation discs, though it is
+ not installed by default. The Command key serves as Meta, but it is
+ reserved for standard Apple shortcuts such as C, V and X, so you must use
+ Esc-C, Esc-V and Esc-X in Emacs or else deselect »Enable key equivalents«
+ in the X11 preferences.</li>
+ <li>The easiest way to install XEmacs or GNU Emacs is via the package manager
+ <a href="http://fink.sourceforge.net/">Fink</a>. Install the Fink package
+ <tt>xemacs-sumo-pkg</tt> to get the XEmacs libraries that Proof General needs
+ to run. To install GNU Emacs, install the package <tt>emacs21</tt>. Fink can
+ compile from sources, but this takes hours, so it is better to request binary
+ installations.</li>
+ <li>To use <a href="http://www.gnu.org/software/emacs/emacs.html">GNU
+ Emacs</a> instead of <a href="http://www.xemacs.org/">XEmacs</a>, you must
+ recompile Proof General and X-Symbol following the instructions <a href=
+ "http://proofgeneral.inf.ed.ac.uk/FAQ">here</a>. Note that Proof General
+ incorporates its own copy of X-Symbol.</li>
+
+ </ul>
+ </ul>
+
+ <p>You may want to install this drag-and-drop <a href=
+ "//dist/misc/isabelle_droplet.dmg">Isabelle launcher</a>. It is a simple hack that
+ invokes XEmacs on any files dropped on it.</p>
+
+ <p>Here is a <a href=
+ "//dist/img/screenshot_isabelle_macos.gif">screenshot</a> showing Proof General running
+ in GNU Emacs.</p>
+
+ </div>
+ <div class="hr"><hr/></div>
+ <?include file="//include/footer.include.html"?>
+</body>
+
+</html>
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/website/installation_notes_cygwin.html Mon Jul 04 15:15:55 2005 +0200
@@ -0,0 +1,265 @@
+<?xml version='1.0' encoding='iso-8859-1' ?>
+<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
+<!-- $Id$ -->
+<html xmlns="http://www.w3.org/1999/xhtml">
+
+<head>
+ <title>Installation notes for Windows/Cygwin</title>
+ <?include file="//include/htmlheader.include.html"?>
+</head>
+
+<body class="dist">
+ <?include file="//include/header.include.html"?>
+ <div class="hr"><hr/></div>
+ <?include file="//include/navigation.include.html"?>
+ <div class="hr"><hr/></div>
+
+ <div id="content">
+
+ <h2>Preconditions and restrictions</h2>
+
+ <p>Please notice before you go ahead:</p>
+
+ <ul>
+ <li>The ML system these notes apply to is <a href=
+ "http://www.smlnj.org/">Standard ML of New Jersey</a>; it is <em>not</em>
+ known yet how to get Isabelle run completely with <a href=
+ "www.polyml.org/">Poly/ML</a>. See <a href="#polyml">a note on Poly/ML</a>
+ down this page.</li>
+
+ <li>It is assumed you have some experience with an Unix operating system
+ (e.g. what a shell is for and how to use it).</li>
+ </ul>
+
+ <p>Any suggestions and improvements concerning this hints are welcomed!</p>
+
+ <h2>Acknowlegements</h2>
+
+ <p>Thanks to <a href=
+ "http://cswww.essex.ac.uk/Research/FSS/projects/isawin/">Norbert
+ Völker</a> and <a href=
+ "http://www.abo.fi/~viorel.preoteasa/isabelle/">Viorel Preoteasa</a> whose
+ efforts helped a lot to get Isabelle run this way.</p>
+
+ <h2>Installing Cygwin</h2>
+
+ <p>Cygwin is a POSIX emulation layer for Windows; it contains ports of a
+ large collection of common Unix software (shells, perl, gcc, X11, latex,
+ ImageMagick, …).</p>
+
+ <p>To install it, get the installer from the <a href=
+ "http://www.cygwin.com">Cygwin website</a> and run it. It will ask you which
+ packages to install, and then downloads and installs them. Please make sure
+ you install everything needed by Isabelle; it is hard to give a concise list
+ of packages here since the bundling of Cygwin packages may vary over time,
+ but installing the base packages, perl, make, xemacs and x-server should be a
+ good choice for the beginning.</p>
+
+ <p>By default, cygwin installs to <tt class="shellcmd">c:\cygwin</tt>; you may choose an
+ arbitrary location, but it is recommended that it does not include any space
+ or exotic characters. This directory will then become the root directory of
+ the Cygwin filesystem tree, i.e. the Cygwin path <tt class="shellcmd">/opt/smlnj</tt> will be
+ mapped to Windows path <tt class="shellcmd">c:\cygwin\opt\smlnj</tt>.</p>
+
+ <p>After installation, open a Cygwin shell window (normally the installer
+ makes a shortcut for you).</p>
+
+ <h2>Getting and building SML/NJ</h2>
+
+ <p>Now we are ready to get and build <a href=
+ "http://www.smlnj.org/">SML/NJ</a>; before this, set the environment variable
+ SMLNJ_CYGWIN_RUNTIME to 1:</p>
+
+ <ul class="shellcmd">
+ <li>export SMLNJ_CYGWIN_RUNTIME=1</li>
+ </ul>
+
+ <p>This setting will tell the build process that it should
+ <em>not</em> attempt to build SML/NJ natively for Win32 but for Cygwin
+ instead (see further <a href=
+ "http://smlnj.cs.uchicago.edu/dist/working/110.53/CYGWININSTALL">CYGWININSTALL</a>).</p>
+
+ <p>So far, this setup was tested using the working version 110.53 of SML/NJ
+ from <a href=
+ "http://smlnj.cs.uchicago.edu/dist/working/110.53/">http://smlnj.cs.uchicago.edu/dist/working/110.53/</a>.
+ SML/NJ provides a nice installer enabling you to download and build it. Read
+ <a href=
+ "http://smlnj.cs.uchicago.edu/dist/working/110.53/INSTALL">INSTALL</a> to
+ learn about the different possibilites to do this. The default packages
+ should be sufficient.</p>
+
+ <p>In the following, it is assumed that you install SML/NJ to Cygwin path
+ <tt class="shellcmd">/opt/smlnj</tt>; if you choose an other location, some tweaking in the
+ <a href="#config"><tt class="shellcmd">etc/settings</tt> file</a> may be neccessary later.</p>
+
+ <p>Whenever SMLNJ is used, the SMLNJ_CYGWIN_RUNTIME environment variable must
+ be set to 1 (later on a convenient mechanism to make this the default is
+ proposed).</p>
+
+ <h2>Installing Isabelle</h2>
+
+ <p>Download the latest Isabelle and ProofGeneral <a href=
+ "download.html">release packages</a>. Assuming that you are in the directory
+ where you downloaded the files, install them into <tt class="shellcmd">/opt</tt> by typing
+ into the bash shell:</p>
+
+ <ul class="shellcmd">
+ <li>tar -C /usr/opt -xvzf <?value key="distname"?>.tar.gz</li>
+ <li>tar -C /usr/opt -xvzf ProofGeneral.tar.gz</li>
+ </ul>
+
+ <p>During extraction, one inconvenience may occur, see <a href=
+ "#inconvenience">below</a>.</p>
+
+ <p>The location <tt class="shellcmd">/opt</tt> again is just a proposal; if you choose other
+ locations, some tweaking in the <a href="#config"><tt class="shellcmd">etc/settings</tt>
+ file</a> may be neccessary later.</p>
+
+ <h2 id="config">Configuring Isabelle</h2>
+
+ <p>Edit the file <tt class="shellcmd">/opt/Isabelle/etc/settings</tt>; first, uncomment the
+ lines about SMLNJ. Also set the variable SMLNJ_CYGWIN_RUNTIME to 1, in order
+ the cygwin version of SMLNJ is used. As mentioned above, the path variables
+ for the ML system and ProofGeneral may need adjustions, depending on your
+ different installation locations.</p>
+
+ <p>Take heed of the setting of ISABELLE_HOME_USER; by default, this is
+ <tt class="shellcmd">~/isabelle</tt>. To detect which Windows path this will be mapped to,
+ type into the Cygwin bash shell:</p>
+
+ <ul class="shellcmd">
+ <li>cygpath --windows ~/isabelle</li>
+ </ul>
+
+ <p>If you don't like this location to be the isabelle home
+ directory, consider setting of ISABELLE_HOME_USER to another value; use
+ <tt class="shellcmd">cygpath --unix <winpath></tt> to detect which Cygwin path a given
+ Windows path is mapped to.</p>
+
+ <p>A typical change could look like this:</p>
+
+ <blockquote>
+ from<br />
+ <tt># Standard ML of New Jersey 110 or later<br />
+ #ML_SYSTEM=smlnj-110<br />
+ #ML_HOME="$ISABELLE_HOME/../smlnj/bin"<br />
+ #ML_OPTIONS="@SMLdebug=/dev/null"<br />
+ #ML_PLATFORM=$(eval $("$ML_HOME/.arch-n-opsys" 2>/dev/null); echo
+ "$HEAP_SUFFIX")<br /></tt>
+ </blockquote>
+
+ <blockquote>
+ to<br />
+ <tt># Standard ML of New Jersey 110 or later<br />
+ SMLNJ_CYGWIN_RUNTIME=1<br />
+ ML_SYSTEM=smlnj-110<br />
+ ML_HOME="$ISABELLE_HOME/../smlnj/bin"<br />
+ ML_OPTIONS="@SMLdebug=/dev/null"<br />
+ ML_PLATFORM=$(eval $("$ML_HOME/.arch-n-opsys" 2>/dev/null); echo
+ "$HEAP_SUFFIX")</tt>
+ </blockquote>
+
+ <h2>Building logics</h2>
+
+ <p>Now we can compile some logics. Start the cygwin shell (if not still
+ running) and type:</p>
+
+ <ul class="shellcmd">
+ <li>cd /opt/Isabelle</li>
+ <li>build HOL</li>
+ <li>build ZF</li>
+ </ul>
+
+ <p>The compilation process may take some time (depending on how fast the
+ computer is). Before building a logic image the build program shows some
+ variables and expects user input – just hit enter.</p>
+
+ <h2>Running Isabelle with ProofGeneral</h2>
+
+ <p>On Linux, Isabelle can be started by two scripts located in
+ <tt class="shellcmd">Isabelle/bin</tt>: <tt class="shellcmd">Isabelle</tt> and <tt class="shellcmd">isabelle</tt>.
+ <tt class="shellcmd">Isabelle</tt> attempts to start ProofGeneral with XEmacs, and isabelle
+ starts it in an SML shell session. However Windows treats the two names as
+ one. To get around this, just rename <tt class="shellcmd">/opt/Isabelle/bin/isabelle</tt> to
+ <tt class="shellcmd">/opt/Isabelle/bin/Isabelle</tt>. This script
+ will start Isabelle with ProofGeneral; the <tt class="shellcmd">isabelle</tt>
+ script in any case is available as <tt class="shellcmd">isabelle-process</tt>.</p>
+
+ <p>Now everything should be ready. To test, start the cygwin shell and
+ type</p>
+
+ <ul class="shellcmd">
+ <li>startx &</li>
+ </ul>
+
+ <p>This will start the cygwin X server and an X shell window. In
+ the X shell window, type</p>
+
+ <ul class="shellcmd">
+ <li>/opt/Isabelle/bin/Isabelle &</li>.
+ </ul>
+
+ <p>This will start the ProofGeneral interface for Isabelle. After a
+ while an empty buffer <tt>Scratch.thy</tt> is created. You can turn on
+ X-Symbol from the menu Proof-General, item Options.</p>
+
+ <p>Load one of your favorite theories and test your Isabelle installation by
+ proving something.</p>
+
+ <p>To simplify starting ProofGeneral, consider writing a Windows command
+ script, e. g.</p>
+
+ <blockquote>
+ <tt>@bash startx -geometry 30x4 -iconic -e Isabell</tt>
+ </blockquote>
+
+ <p>and assigning a shortcut in the start menu to it.</p>
+
+ <h2 id="inconvenience">Inconveniencies with the current version of
+ Isabelle</h2>
+
+ <p>With the current Isabelle release (Isabelle 2004), there are two
+ inconveniencies:</p>
+
+ <ul>
+ <li>During extraction you will get a warning that file
+ <tt class="shellcmd">Real/HahnBanach/Aux.thy</tt> can not be created. This is because
+ <tt class="shellcmd">Aux</tt> is not allowed as a filename under Windows. If you do not want
+ to run the HahnBanach example, you might simply want to ignore this
+ warning.</li>
+
+ <li>The tool <tt class="shellcmd">isatool mkdir</tt> tries to detect the name of the current
+ user, to put it into the generated <tt class="shellcmd">root.tex</tt>. Alas, on Windows,
+ this leads to an unquoted <tt>\</tt> in the TeX file. So you either must
+ edit your <tt class="shellcmd">root.tex</tt> manually to fix this, or directly patch
+ <tt class="shellcmd">/opt/Isabelle/lib/Tools/mkdir</tt> by replacing
+
+ <blockquote>
+ <tt>AUTHOR=$("$AUTO_PERL" -e "@pw = getpwnam(\"$USER\"); print @pw[6]" | tr _ -)</tt>
+ </blockquote>with
+
+ <blockquote>
+ <tt>AUTHOR="default author name"</tt>
+ </blockquote>
+ </li>
+ </ul>
+
+ <p>To get around these inconveniencies, consider using a recent developer
+ snapshot of Isabelle; both will be fixed in the next Isabelle release.</p>
+
+ <h2 id="polyml">A note on Poly/ML</h2>
+
+ <p>As indicated above, Isabelle does <em>not</em> run neatly with <a href=
+ "http://www.polyml.org/">Poly/ML</a> on Windows, since it is not clear
+ how Poly/ML has to be compiled for Cygwin, and the native Windows port
+ of PolyML does not provide some Posix signals Isabelle/ProofGeneral relies on.</p>
+
+ <p>If you know how to circumvent (fully or partially) any of these problems,
+ please let us know.</p>
+
+ </div>
+ <div class="hr"><hr/></div>
+ <?include file="//include/footer.include.html"?>
+</body>
+
+</html>
--- a/Admin/website/overview.html Mon Jul 04 14:42:06 2005 +0200
+++ b/Admin/website/overview.html Mon Jul 04 15:15:55 2005 +0200
@@ -14,8 +14,7 @@
<?include file="//include/navigation.include.html"?>
<div class="hr"><hr/></div>
<div id="content">
- <?include file="//include/mirrorlist.major.include.html"?>
- <div class="hr"><hr/></div>
+
<h2>What is Isabelle?</h2>
<p>
Isabelle is a generic proof assistant. It allows mathematical
@@ -39,7 +38,7 @@
<p>Isabelle is distributed <em>freely</em> under the open source
<!--a href="//dist/packages/Isabelle/COPYRIGHT"-->BSD license<!--/a-->.
- You may use any of our <a href="dist/index.html">mirrors</a> for download.</p>
+ You may use any of our <a href="mirrors.html">mirrors</a> for download.</p>
<h2>Preview of Isabelle</h2>
@@ -87,7 +86,7 @@
"http://proofgeneral.inf.ed.ac.uk/">ProofGeneral</a> user interface, which
eases the task of writing and maintaining proof scripts.</p>
- <p>Ample <a href="dist/documentation.html">documentation</a> is available
+ <p>Ample <a href="documentation.html">documentation</a> is available
about using Isabelle and its inner concepts, including a
<a href="http://www4.in.tum.de/~nipkow/LNCS2283/">Tutorial</a> published by
Springer-Verlag.</p>
--- a/Admin/website/packages.html Mon Jul 04 14:42:06 2005 +0200
+++ b/Admin/website/packages.html Mon Jul 04 15:15:55 2005 +0200
@@ -8,15 +8,13 @@
<?include file="//include/htmlheader.include.html"?>
</head>
-<body class="dist">
+<body>
<?include file="//include/header.include.html"?>
<div class="hr"><hr/></div>
<?include file="//include/navigation.include.html"?>
<div class="hr"><hr/></div>
<div id="content">
- <?include file="//include/mirrorlist.include.html"?>
- <div class="hr"><hr/></div>
<h2><?value key="distname"?></h2>