# HG changeset patch
# User haftmann
# Date 1119967923 -7200
# Node ID e7df213a1918b933437c073733a743e03e60810d
# Parent  5854996e6060e554523ba4fee1f3b595ac5bb811
added project information in overview

diff -r 5854996e6060 -r e7df213a1918 Admin/website/TODO
--- 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
diff -r 5854996e6060 -r e7df213a1918 Admin/website/community.html
--- 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="&#109;&#97;&#105;&#108;&#116;&#111;:&#105;&#115;&#97;&#98;&#101;&#108;&#108;&#101;-&#117;&#115;&#101;&#114;&#115;&#64;&#99;&#108;&#46;&#99;&#97;&#109;&#46;&#97;&#99;&#46;&#117;&#107;">&#105;&#115;&#97;&#98;&#101;&#108;&#108;&#101;-&#117;&#115;&#101;&#114;&#115;&#64;&#99;&#108;&#46;&#99;&#97;&#109;&#46;&#97;&#99;&#46;&#117;&#107;</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
diff -r 5854996e6060 -r e7df213a1918 Admin/website/dist/installation.html
--- 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>
diff -r 5854996e6060 -r e7df213a1918 Admin/website/dist/installation_notes_cygwin.html
--- 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 &amp;</li>.
+        <li>/opt/Isabelle/bin/Isabelle &amp;</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.&nbsp;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>
diff -r 5854996e6060 -r e7df213a1918 Admin/website/faq.html
--- 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>
diff -r 5854996e6060 -r e7df213a1918 Admin/website/index.html
--- 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. 
diff -r 5854996e6060 -r e7df213a1918 Admin/website/overview.html
--- 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