--- a/Admin/website/TODO Tue Jun 28 16:12:03 2005 +0200
+++ b/Admin/website/TODO Tue Jun 28 16:12:03 2005 +0200
@@ -1,12 +1,5 @@
For the next release:
-- better argument handling in pypager --> test it
-
-- centralize scattered project partners informations at "community"
-- move projects from "overview" to "community"
-
-- reduce prominence of license issue at "overview"
-
- add CONTRIBUTORS and COPYRIGHT to Packages
- clarify purpose of the rsync daemon, consider
--- a/Admin/website/community.html Tue Jun 28 16:12:03 2005 +0200
+++ b/Admin/website/community.html Tue Jun 28 16:12:03 2005 +0200
@@ -15,9 +15,21 @@
<div class="hr"><hr/></div>
<div id="content">
+ <h2>Project partners</h2>
+
+ <p>Isabelle is a joint project between
+ <a href="http://www.cl.cam.ac.uk/users/lcp/">Larry Paulson</a>
+ (<a href="http://www.cl.cam.ac.uk/Research/HVG/Isabelle/cambridge.html">University of Cambridge</a>, UK) and
+ <a href="http://www.in.tum.de/~nipkow/">Tobias Nipkow</a>
+ (<a href="http://www4.in.tum.de/proj/theoremprov/group.html">Technical University of Munich</a>, Germany).</p>
+
+ <p>There is an (incomplete) list of past and present <a href=
+ "http://www.cl.cam.ac.uk/Research/HVG/Isabelle/projects.html">projects</a>
+ undertaken using Isabelle.</p>
+
<h2>Mailing list</h2>
- <p>
- You may use the mailing list <a
+
+ <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
@@ -39,6 +51,7 @@
<a href="http://afp.sf.net">Archive of Formal Proofs</a>.</p>
<h2 id="afp">The Archive of Formal Proofs (AFP)</h2>
+
<p>The <a href="http://afp.sf.net">Archive of Formal Proofs</a> is a collection of proof
libraries, examples, and larger scientifc developments, mechanically checked
in Isabelle. It is organized in the way of a scientific journal. Submissions
--- a/Admin/website/dist/installation.html Tue Jun 28 16:12:03 2005 +0200
+++ b/Admin/website/dist/installation.html Tue Jun 28 16:12:03 2005 +0200
@@ -19,9 +19,8 @@
<p>
Isabelle runs on common Unix platforms.
- For Linux and Solaris, we provide ready-to-install bundles;
+ For Linux, Solaris and MaxOS / Darwin, we provide ready-to-install bundles;
for other Unices, Isabelle has to be built from scratch.
- We provide also some hints on how to use Isabelle on other, not-quite-Unix platforms.
</p>
<p>
@@ -44,7 +43,7 @@
<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_cygwin">Windows / Cygwin</a></li>
+ <li><a href="#install_windows">Windows</a></li>
</ul>
<h2 id="install_linux">Linux</h2>
@@ -183,14 +182,15 @@
</li>
</ul>
- <h2 id="install_cygwin">Windows / Cygwin</h2>
+ <h2 id="install_windows">Windows</h2>
- <p>See <a href="installation_notes_cygwin.html">Installation notes for
+ <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>Those
- installation instructions are hints contributed by
- Isabelle users. Please feel free to contact us for any suggestions,
- corrections or improvements.</p>
+
+ <p>For a serious apporach, you should consider a Windows/Linux dualboot
+ installation.</p>
</div>
<div class="hr"><hr/></div>
--- a/Admin/website/dist/installation_notes_cygwin.html Tue Jun 28 16:12:03 2005 +0200
+++ b/Admin/website/dist/installation_notes_cygwin.html Tue Jun 28 16:12:03 2005 +0200
@@ -29,7 +29,9 @@
<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=
@@ -177,9 +179,10 @@
<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 copy <tt class="shellcmd">/opt/Isabelle/bin/isabelle</tt> to
- <tt class="shellcmd">/opt/Isabelle/bin/Isabell</tt>. The script
- <tt class="shellcmd">/opt/Isabelle/bin/Isabell</tt> will start Isabelle with ProofGeneral.</p>
+ 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>
@@ -192,7 +195,7 @@
the X shell window, type</p>
<ul class="shellcmd">
- <li>/opt/Isabelle/bin/Isabell &</li>.
+ <li>/opt/Isabelle/bin/Isabelle &</li>.
</ul>
<p>This will start the ProofGeneral interface for Isabelle. After a
@@ -203,7 +206,7 @@
proving something.</p>
<p>To simplify starting ProofGeneral, consider writing a Windows command
- script, e.g.</p>
+ script, e. g.</p>
<blockquote>
<tt>@bash startx -geometry 30x4 -iconic -e Isabell</tt>
@@ -248,7 +251,7 @@
<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 do not provide some Posix interfaces Isabelle relies on.</p>
+ 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>
--- a/Admin/website/faq.html Tue Jun 28 16:12:03 2005 +0200
+++ b/Admin/website/faq.html Tue Jun 28 16:12:03 2005 +0200
@@ -259,13 +259,6 @@
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>Does Isabelle run on Windows?</dt>
-
- <dd>After a fashion, yes, but Isabelle is not being developed for
- Windows. See the <a href="dist/installation_notes_cygwin.html">installation notes</a> for windows.
- If the approach presented there is not sufficient for your purpose, consider a
- dualboot Windows/Linux system.</dd>
-
</dl>
</div>
--- a/Admin/website/index.html Tue Jun 28 16:12:03 2005 +0200
+++ b/Admin/website/index.html Tue Jun 28 16:12:03 2005 +0200
@@ -44,7 +44,6 @@
bibliography, and Isabelle workshops and courses.
</p>
-
<h2>Coming soon: Isabelle 2005</h2>
<p>New features in the upcoming Isabelle 2005 will include</p>
<ul>
@@ -101,8 +100,8 @@
<h2>Download</h2>
<p>
-The Isabelle distribution is available
-from several <a href="dist/index.html">mirror sites</a>. It includes
+The Isabelle distribution is distributed <em>for free</em> and available
+from several <a href="dist/index.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/overview.html Tue Jun 28 16:12:03 2005 +0200
+++ b/Admin/website/overview.html Tue Jun 28 16:12:03 2005 +0200
@@ -85,7 +85,6 @@
<p>Isabelle is closely integrated with the <a href=
"http://proofgeneral.inf.ed.ac.uk/">ProofGeneral</a> user interface, which
eases the task of writing and maintaining proof scripts.</p>
- <br clear="all" />
<p>Ample <a href="dist/documentation.html">documentation</a> is available
about using Isabelle and its inner concepts, including a