# HG changeset patch # User kleing # Date 1115595546 -7200 # Node ID 07a791202f493bfcb51bcdef2256b10bc97a8dba # Parent d84d5e4e7c714d3a374e9648e10eadc9fff1dab1 made download links local, provide explicit list of files to download diff -r d84d5e4e7c71 -r 07a791202f49 Admin/page/dist-content/notes_macos_darwin.content --- a/Admin/page/dist-content/notes_macos_darwin.content Mon May 09 01:32:47 2005 +0200 +++ b/Admin/page/dist-content/notes_macos_darwin.content Mon May 09 01:39:06 2005 +0200 @@ -17,20 +17,15 @@ OS X developer tools.

    -
  1. Download Isabelle to a suitable directory, as described on the download -page. -Ensure that you get files such as -polyml_ppc-darwin.tar.gz and -HOL_ppc-darwin.tar.gz rather than the _x86-linux -versions.
    2. +
  2. Download Isabelle to a suitable directory, as described on the +download page. Be sure to get the following files -
  3. Install Poly/ML in a standard -place, such as /usr/local/polyml, or put polyml in the -same directory as Isabelle. Make sure you get the PPC Darwin -version from the Poly/ML download page.
    4. +
    +
    +
    +
    +
    +
  4. 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 @@ -42,19 +37,20 @@ following the instructions for "Compiling Logics" in file Isabelle/INSTALL.
    5. -
  5. Install Proof General. -You may now be able to launch Proof General by typing "Isabelle" -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 You should also be able to launch Proof General by typing +"Isabelle" 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 MacEmacs JP or -mindlube's or Enhanced Carbon Emacs. -Visiting a theory file from Emacs will automatically launch Proof General -provided isabelle is on the search path. None of these options -support the X-Symbol package, unfortunately.
    6. -
+mindlube's or Enhanced Carbon +Emacs. Visiting a theory file from Emacs will automatically +launch Proof General provided isabelle is on the search +path. None of these options support the X-Symbol package, +unfortunately.

In order to get the full benefit of Proof General, you must install the X Window System (X11) and XEmacs or