Return-Path: Delivery-Date: Received: from dworshak.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Thu, 16 Sep 1993 13:48:09 +0100 Received: by dworshak.cs.uidaho.edu (1.37.109.4/16.2) id AA08962; Thu, 16 Sep 93 05:35:56 -0700 Sender: info-hol-request@cs.uidaho.edu Errors-To: info-hol-request@cs.uidaho.edu Precedence: bulk Received: from achernar.anu.edu.au by dworshak.cs.uidaho.edu with SMTP (1.37.109.4/16.2) id AA08958; Thu, 16 Sep 93 05:35:33 -0700 Received: by achernar.anu.edu.au id AA00667 (5.65c/IDA-1.4.4 for info-hol@cs.uidaho.edu); Thu, 16 Sep 1993 22:33:08 +1000 Date: Thu, 16 Sep 1993 22:33:08 +1000 From: Malcolm Newey Message-Id: <199309161233.AA00667@achernar.anu.edu.au> To: slind@informatik.tu-muenchen.de Subject: Re: postscript versions of HOL docs? Cc: info-hol@cs.uidaho.edu Hi Konrad, You write: > > Someone interested in running hol90 on a Mac writes, in reference to the > HOL manuals: > > > I was also wondering if there is any way I can print all those LaTeX > > manuals to my PostScript printer. Is there any way to run LaTeX without > > UNIX, such as a Macintosh version of UNIX? > > Are the HOL manuals available in Postscript format? > I think both you and your correspondent ask the wrong question! I say this because every HOL user can make good use of the HOL LaTex macros that come with the system to make lists of theorems more readable. There are two versions of LaTex for the Mac that are well-known in TeX circles: - A commercial product called Textures - A free product (that some say is better) called OzTex The latter happens to originate at here at ANU but is readily available at a number of sites worldwide. The following comes from the TeX FAQ: ...... 7) What is OzTeX and where can I get it (TeX for the Mac)? OzTeX is a public domain version of TeX for the Macintosh. A DVI Previewer and PostScript driver are also included. It should run on any Macintosh Plus, SE, II, or newer model, but will not work on a 128K or 512K Mac. It was written by Andrew Trevorrow, and is available via anonymous ftp from from midway.uchicago.edu (128.135.12.73) in ./pub/OzTeX, which contains other public domain TeX-related software for the Mac as well, or on a floppy disk from TUG (see question 11). Questions about OzTeX may be directed to oztex@midway.uchicago.edu. 8) ....... Now I'm told that this FAQ sheet is out of date. The arrival of CTAN changes the picture. My informant says: CTAN (comprehensive tex archive network) has been set up. These archive sites are the definitve TeX sources. It would be wisest to get ozTeX from there, particularly if the person you are advising is not local. CTAN sites: ftp.shsu.edu /tex-archive ftp.tex.ac.uk /pub/archive ftp.uni-stuttgart.de /soft/tex on any of these, oztex is found in systems/mac/ I note that in that dir there are is also oztex-german and euro-oztex, which may be useful (or not!).