added notes for mac os

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/page/dist-content/notes_macos_darwin.content	Fri May 06 16:03:56 2005 +0200
@@ -0,0 +1,102 @@
+%title%
+Isabelle under Mac OS X
+
+%body%
+
+<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="isabelle_macos_screenshot.jpg">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 download
+<a href=
+"http://www.cl.cam.ac.uk/Research/HVG/Isabelle/dist/packages.html">page</a>.
+Ensure that you get files such as <a href=
+"http://www.cl.cam.ac.uk/Research/HVG/Isabelle/dist/contrib/polyml_ppc-darwin.tar.gz">
+<tt>polyml_ppc-darwin.tar.gz</tt></a> and <a href=
+"http://www.cl.cam.ac.uk/Research/HVG/Isabelle/dist/HOL_ppc-darwin.tar.gz"><tt>
+HOL_ppc-darwin.tar.gz</tt></a> rather than the <tt>_x86-linux</tt>
+versions.</li>
+
+<li>Install <a href="http://www.polyml.org/">Poly/ML</a> in a standard
+place, such as <tt>/usr/local/polyml</tt>, or put <tt>polyml</tt> in the
+same directory as <tt>Isabelle</tt>. Make sure you get the PPC Darwin
+version from the Poly/ML download page.</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>Isabelle/INSTALL.</tt></li>
+
+<li>Install <a href="http://proofgeneral.inf.ed.ac.uk/">Proof General</a>.
+You may now be able to launch Proof General by typing "<tt>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>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>
+

--- a/Admin/page/dist-content/packages.content	Fri May 06 15:00:08 2005 +0200
+++ b/Admin/page/dist-content/packages.content	Fri May 06 16:03:56 2005 +0200
@@ -128,12 +128,21 @@
 <A HREF="http://proofgeneral.inf.ed.ac.uk/FAQ">Proof General FAQ</a> 
 for advice.
 
-<h3>Running Isabelle on windows</h3>
+<h3>Running Isabelle on non-unix operating systems.</h3>
 
-<p>For a complete system, we recommend to run some recent version of
-Solaris, Darwin, or Linux.</p>
+<p>Though Isabelle is nativly designed for Unix (e.&nbsp;g. Solaris, Linux),
+Isabelle may also run under similar &raquo;unix-like&laquo; platforms:
 
-<p>Though not &raquo;officially supported&laquo;, Isabelle in most
-cases should also run on Windows, using the
-<a href="http://www.cygwin.com/">Cygwin</a> POSIX emulation layer. Here
-some <a href="notes_win_cygwin.html">notes</a> about it.</p>
+    <ul>
+        <li>Max OS X, since the Darwin kernel is a Unix kernel; see
+        <a href="notes_macos_darwin.html">installation notes for Max OS</a>.</li>
+        <li>Windows, using the <a href="http://www.cygwin.com/">Cygwin</a>
+        POSIX emulation layer; see <a href="notes_win_cygwin.html">installation
+        notes for Cygwin/Windows</a>.</li>
+    </ul>
+
+</p>
+
+<p>These installation instructions are not strictly normative, they are just
+hints contributed by Isabelle users.
+Feel free to contact us for any suggestions, corrections or improvements.</p>