--- a/Admin/website/documentation.html Mon Sep 26 20:51:57 2005 +0200
+++ b/Admin/website/documentation.html Mon Sep 26 20:52:36 2005 +0200
@@ -55,8 +55,8 @@
<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> -->
+ <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>
--- a/Admin/website/download_past.html Mon Sep 26 20:51:57 2005 +0200
+++ b/Admin/website/download_past.html Mon Sep 26 20:52:36 2005 +0200
@@ -21,6 +21,7 @@
Past releases of Isabelle are available from the Cambridge
archive:
<ul>
+ <li><a href="http://www.cl.cam.ac.uk/users/lcp/archive/Isabelle2004.tar.gz">Isabelle2004</a></li>
<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>
--- a/Admin/website/faq.html Mon Sep 26 20:51:57 2005 +0200
+++ b/Admin/website/faq.html Mon Sep 26 20:52:36 2005 +0200
@@ -37,15 +37,15 @@
<dt>Is it available for download?</dt>
<dd>Yes, it is available from several mirror sites, e. g. from
- <a href="http://isabelle.in.tum.de">Munich</a>. It should run
- on most recent Unix systems (Solaris, Linux, MacOS X, etc.).</dd>
+ <a href="http://isabelle.in.tum.de">Munich</a>. It runs on common
+ Unix systems (Linux, MacOS X, Solaris, etc.).</dd>
</dl>
<h2>Syntax</h2>
<dl class="faq">
- <dt>There are lots of arrows in Isabelle. What's the difference between
+ <dt>There are lots of arrows in Isabelle/HOL. What's the difference between
<tt>-></tt>, <tt>=></tt>, <tt>--></tt>, and <tt>==></tt>
?</dt>
@@ -81,7 +81,7 @@
the constructors in the case pattern is different from the order in which
they where defined (in the datatype definition).</dd>
- <dt>Why doesn't Isabelle understand my equation?</dt>
+ <dt>Why doesn't Isabelle/HOL understand my equation?</dt>
<dd>Isabelle's equality <tt>=</tt> binds relatively strongly, so an
equation like <tt>a = b & c</tt> might not be what you intend.
@@ -94,7 +94,7 @@
<dd>Most commonly this is an instance of the question above. The
<tt>primrec</tt> command (and others) expect equations as input, and
- since equality binds strongly in Isabelle, something like <tt>f x = b
+ since equality binds strongly in Isabelle/HOL, something like <tt>f x = b
& c</tt> is not what you might expect it to be: Isabelle parses it as
<tt>(f x = b) & c</tt> (which is indeed not a proper equation). To
turn it into an equation you must set explicit parentheses: <tt>f x = (b
@@ -141,10 +141,10 @@
<dt>Why does <tt>lemma "1+1=2"</tt> fail?</dt>
- <dd>Because it is not necessarily true. Isabelle does not assume that 1
+ <dd>Because it is not necessarily true. Isabelle/HOL does not assume that 1
and 2 are natural numbers. Try <tt>"(1::nat)+1=2"</tt> instead.</dd>
- <dt>Can Isabelle find counterexamples?</dt>
+ <dt>Can Isabelle/HOL find counterexamples?</dt>
<dd>
<p>For arithmetic goals, <code>arith</code> finds counterexamples. For
@@ -168,41 +168,6 @@
<dl class="faq">
- <dt>ProofGeneral appears to hang when Isabelle is started.</dt>
- <dd><p>This may be because of UTF-8 issues e.g. in Red Hat 8.0/9.0, Suse
- 9.0/9.1</p>
- <p>RedHat 8 and later has glibc 2.2 and UTF8 encoded output may be turned on
- in default locale. Unfortunately Proof General relies on 8-bit characters
- which are UTF8 prefixes in the output of proof assistants (inc Coq,
- Isabelle). These prefix characters are not flushed to stdout individually. As
- a workaround we must find a way to disable interpretation of UTF8 in the C
- libraries that Coq and friends use.</p>
-
- <p>Doing this inside PG/Emacs seems tricky; locale settings are set/inherited
- in strange ways. One solution is to run the Emacs process itself with an
- altered locale setting, for example, starting XEmacs by typing:</p>
-
- <ul class="shellcmd">
- <li>LC_CTYPE=en_GB Isabelle &</li>
- </ul>
-
- <p>The supplied proofgeneral script makes this setting if it sees the string
- UTF in the current value of <tt class="shellcmd">LC_CTYPE</tt>.
- Depending on your distribution, this
- variable might also be called <tt class="shellcmd">LANG</tt>.</p>
-
- <p>Alternatively you can set <tt class="shellcmd">LC_CTYPE</tt> or
- <tt class="shellcmd">LANG</tt> inside a file <tt class="shellcmd">~/.i18n</tt>, which
- will be read by the shell. This will affect all applications, though.</p>
-
- <p>Suggestions for a better workaround inside Emacs would be welcomed;</p>
-
- <p>A related issue is warnings from x-symbol: "Emacs language environment
- and system locale specify different encoding, I'll assume `iso-8859-1'". This
- warning appears to be mainly harmless. Notice that the variable
- `buffer-file-coding-system' may determine the format that files are saved
- in.</p></dd>
-
<dt>X-Symbol doesn't seem to work. What can I do?</dt>
<dd>The most common reason why X-Symbol doesn't work is: it's not
@@ -211,7 +176,7 @@
select the menu items <tt>Proof-General -> Options -> X-Symbol</tt>
and (if you want to save the setting for future sessions) select
<tt>Options -> Save Options</tt> in XEmacs.</dd>
-
+
<dt>How do I input those X-Symbols anyway?</dt>
<dd>There are lots of ways to input x-symbols. The one that always works
@@ -258,6 +223,17 @@
create an image <tt class="shellcmd">MyImage</tt> using the parent logic <tt class="shellcmd">HOL</tt>. You
should then be able to invoke Isabelle with <tt class="shellcmd">Isabelle -l MyImage</tt>
and have everything that is loaded in ROOT.ML instantly available.</dd>
+
+ <dt>Can I run Isabelle on Windows?</dt>
+
+ <dd>Not really. The Cygwin environment provides a Unixoid
+ look-and-feel that is sufficient for very basic Isabelle
+ functionality. See also <a
+ href="installation_notes_cygwin.html">Installation notes for
+ Cygwin/Windows.</a>
+
+ To try out Isabelle it might be much easier to use a Linux boot
+ CD, such as <a href="http://www.knoppix.org/">Knoppix</a>.</dd>
</dl>
--- a/Admin/website/include/downloadtable.include.html Mon Sep 26 20:51:57 2005 +0200
+++ b/Admin/website/include/downloadtable.include.html Mon Sep 26 20:52:36 2005 +0200
@@ -7,37 +7,31 @@
<td>
Sources and documentation
</td>
- <?downloadCells target="//dist/packages/Isabelle2004.tar.gz" title="Isabelle2004.tar.gz"?>
+ <?downloadCells target="//dist/packages/Isabelle2005.tar.gz" title="Isabelle2005.tar.gz"?>
</tr>
<tr>
<td>
Documentation in PDF
</td>
- <?downloadCells target="//dist/packages/Isabelle2004_pdf.tar.gz" title="Isabelle2004_pdf.tar.gz"?>
+ <?downloadCells target="//dist/packages/Isabelle2005_pdf.tar.gz" title="Isabelle2005_pdf.tar.gz"?>
</tr>
<tr>
<td>
Theory library in PDF and HTML
</td>
- <?downloadCells target="//dist/packages/Isabelle2004_library.tar.gz" title="Isabelle2004_library.tar.gz"?>
+ <?downloadCells target="//dist/packages/Isabelle2005_library.tar.gz" title="Isabelle2005_library.tar.gz"?>
</tr>
<tr><td colspan="3" class="downloadheader">Proof General</td></tr>
<tr>
<td>
Proof General
</td>
- <?downloadCells target="//dist/packages/contrib/ProofGeneral-3.5.tar.gz" title="ProofGeneral-3.5.tar.gz"?>
+ <?downloadCells target="//dist/packages/contrib/ProofGeneral.tar.gz" title="ProofGeneral.tar.gz"?>
</tr>
<tr><td colspan="3" class="downloadheader">Poly/ML compiler and runtime system</td></tr>
<tr>
- <td>
- Poly/ML base system
- </td>
- <?downloadCells target="//dist/packages/contrib/polyml_base.tar.gz" title="polyml_base.tar.gz"?>
- </tr>
- <tr>
<td rowspan="3">
- Poly/ML binary modules
+ Poly/ML
</td>
<?downloadCells target="//dist/packages/contrib/polyml_x86-linux.tar.gz" title="polyml_x86-linux.tar.gz"?>
</tr>
@@ -114,4 +108,3 @@
<?downloadCells target="//dist/packages/contrib/HOL4-proofs.tar.gz" title="HOL4-proofs.tar.gz"?>
</tr>
</table>
-
--- a/Admin/website/index.html Mon Sep 26 20:51:57 2005 +0200
+++ b/Admin/website/index.html Mon Sep 26 20:52:36 2005 +0200
@@ -44,67 +44,28 @@
bibliography, and Isabelle workshops and courses.
</p>
- <h2>Coming soon: Isabelle 2005</h2>
- <p>New features in the upcoming Isabelle 2005 will include</p>
+ <h2>Now available: Isabelle 2005</h2>
+ <p>Some notable highlights:</p>
<ul>
- <li>New commands for instantiating locales</li>
- <li>New command for finding theorems (by term patterns, as intro/elim/simp rules, etc.)</li>
- <li>New automatic transitivity reasoner</li>
- <li>New command for ad-hoc theory viewing and printing</li>
- <li>Much extended and improved theory of finite sets</li>
- <li>New syntax that will allow > and >= in addition to < and
- <=</li>
- </ul>
-
- <h2>Isabelle 2004</h2>
-
-<p>New features in Isabelle 2004 include</p>
-
-<ul>
-<li>New image HOL4 with imported library from HOL4 system on top of
- HOL-Complex (about 2500 additional theorems).</li>
-
-<li>New theory Ring_and_Field with over 250 basic numerical laws,
- all proved in axiomatic type classes for semirings, rings and fields.</li>
-
-<li>New locale <code>ring</code> for non-commutative rings in HOL-Algebra.</li>
+ <li>Interpretation of locale expressions in theories, locales, and proof contexts.</li>
+ <li>Substantial library improvements (HOL, HOL-Complex, HOLCF).</li>
+ <li>Proof tools for transitivity reasoning.</li>
+ <li>General <code>find_theorems</code> command (by term patterns, as intro/elim/simp rules etc.).</li>
+ <li>Commands for generating adhoc draft documents.</li>
+ <li>Support for Unicode proof documents (UTF-8).</li>
+ <li>Major internal reorganizations and performance improvements.</li>
+ </ul>
-<li>Type <code>rat</code> of the rational numbers available in HOL-Complex.</li>
-
-<li>New theory of matrices with an application to linear programming in HOL-Matrix.</li>
-
-<li>Improved locales (named proof contexts), instantiation of locales.</li>
-
-<li>Improved handling of linear and partial orders in simplifier.</li>
-
-<li>New <code>specification</code> command for definition by specification.</li>
-
-<li>New Isar command <code>finalconsts</code> prevents constants being given a definition later.</li>
-
-<li><code>arith</code> now generates counterexamples for reals as well.</li>
-
-<li>New <code>quickcheck</code> command
- to search for counterexamples of executable goals.
- (see HOL/ex/Quickcheck_Examples.thy)</li>
-<li>New <code>refute</code> command
- to search for finite countermodels of goals.
- (see HOL/ex/Refute_Examples.thy)
-</li>
-
-<li>Presentation and x-symbol enhancements, greek letters and
-sub/superscripts allowed in identifiers.</li>
-</ul>
-
-<p><a href="//dist/packages/Isabelle/NEWS">[Complete Changelog]</a></p>
+<p><a href="//dist/packages/Isabelle/NEWS">[Cumulative NEWS]</a></p>
<h2>Download</h2>
<p>
-The Isabelle distribution is distributed for free under the BSD license.
-It includes source and binary packages and browsable documentation,
-see the <a href="installation.html">installation instructions</a>. You can also
-browse the <a href="//dist/library/index.html">Isabelle theory library</a>
-online.
+Isabelle is distributed for free under the BSD license. It includes
+source and binary packages and browsable documentation, see the <a
+href="installation.html">installation instructions</a>. You can also
+browse the <a href="//dist/library/index.html">Isabelle theory
+library</a> online.
</p>
<p>
--- a/Admin/website/installation.html Mon Sep 26 20:51:57 2005 +0200
+++ b/Admin/website/installation.html Mon Sep 26 20:52:36 2005 +0200
@@ -19,19 +19,22 @@
<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.
+ Isabelle runs on common Unix platforms. We provide
+ ready-to-use binary packages for Linux/x86, MaxOS X /
+ Darwin, and Solaris. For other platforms, Isabelle logics
+ need to be compiled separately (see also <a
+ href="//dist/packages/Isabelle/INSTALL">INSTALL</a>).
</p>
<p>
- A usable Isabelle system consists of the following components:
+ A practically 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 Isabelle system itself, including the desired object logics
+ (e. g. HOL, HOL-Complex)</li>
<li>the ProofGeneral user interface</li>
</ul>
@@ -42,157 +45,130 @@
<ul>
<li><a href="#install_linux">Linux (x86)</a></li>
+ <li><a href="#install_darwin">MacOS X / Darwin (ppc)</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>
+ <p>Installation of Isabelle/HOL on common Linux/x86 platforms
+ works 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>For ProofGeneral, ensure that your system has a
+ working installation of XEmacs 21, or Emacs 21 with
+ mule support. The XEmacs 21.1.x and 21.4.x versions
+ are known to work reasonably well, but the beta branch
+ of XEmacs 21.5.x usually fails!</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>
+ and Isabelle – all of this is available from the
+ Isabelle <a href="download.html">Packages</a> page.
+ When you download ProofGeneral for the first time,
+ please <a
+ href="http://proofgeneral.inf.ed.ac.uk/register">register</a>.</li>
+
+ <li>Likewise download the compiled images of the desired
+ Isabelle object logics.</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>
+ <li>tar -C /usr/local -xzf <?downloadLink target="//dist/packages/Isabelle2005.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>
+ <li>tar -C /usr/local -xzf <?downloadLink target="//dist/packages/contrib/ProofGeneral.tar.gz"?></li>
</ul>
</li>
- <li>Under most circumstances, the default settings of Isabelle should be reasonable for
- invoking Isabelle/ProofGeneral without further ado:
+
+ <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.
+
+ Failure on this is typically a problem with unstable
+ XEmacs versions; consider command line option
+ <code>-p</code> to specify a different xemacs
+ executable.
+
+ The X-Symbol package is already included in Proof
+ General, but needs to be enabled separately; use the
+ <code>-x</code> command line option, or the
+ <em>Options</em> menu.
</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>Ensure that your system provides the following:</p>
+ <ul>
+ <li>MacOS X 10.2.2 or higher</li>
+
+ <li>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 installation on MacOS X / Darwin is analogous to
+ Linux, but note that some GNU executables are named
+ differently.</p>
+
+ <ul>
+ <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/Isabelle2005.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_ppc-darwin.tar.gz"?></li>
+ <li>gtar -C /usr/local -xzf <?downloadLink target="//dist/packages/HOL_ppc-darwin.tar.gz"?></li>
+ </ul>
+ </li>
+
+ <li>Invoke Isabelle/ProofGeneral as follows:
+ <ul class="shellcmd">
+ <li>/usr/local/Isabelle/bin/Isabelle</li>
+ </ul>
+ </li>
+
+ </ul>
<h2 id="install_solaris">Solaris</h2>
- <p>Before you start, ensure the following for your system:</p>
+ <p>Ensure that the following tools are available on your system:</p>
<ul>
+ <li>Perl 5.x</li>
<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>
+ <li>XEmacs 21, or Emacs 21 with mule support (for ProofGeneral)</li>
</ul>
- <p>Then, an installation on Solaris is analogous to Linux:</p>
+ <p>The rest of the installation is analogous to Linux (see
+ above).</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/Isabelle2005.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:
+
+ <li>Invoke Isabelle/ProofGeneral as follows:
<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"?>
--- a/Admin/website/overview.html Mon Sep 26 20:51:57 2005 +0200
+++ b/Admin/website/overview.html Mon Sep 26 20:52:36 2005 +0200
@@ -36,9 +36,10 @@
(University of Cambridge, UK) and Tobias Nipkow (Technical
University of Munich, Germany).</p>
- <p>Isabelle is distributed <em>freely</em> under the open source
- <!--a href="//dist/packages/Isabelle/COPYRIGHT"-->BSD license<!--/a-->;
- see the <a href="installation.html">installation instructions</a>.</p>
+ <p>Isabelle is distributed <em>freely</em> as Open Source
+ Software <!--a href="//dist/packages/Isabelle/COPYRIGHT"-->BSD
+ license<!--/a-->; see the <a
+ href="installation.html">installation instructions</a>.</p>
<h2>Preview of Isabelle</h2>
--- a/Admin/website/packages.html Mon Sep 26 20:51:57 2005 +0200
+++ b/Admin/website/packages.html Mon Sep 26 20:52:36 2005 +0200
@@ -20,7 +20,7 @@
<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,
+ working environment on common Unix platforms (e.g. Linux, MacOS X,
Solaris). We provide a complete set of packages for Isabelle, Proof
General, and PolyML.</p>