Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Sat, 1 May 1993 11:58:41 +0100 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA05315; Fri, 30 Apr 93 14:37:34 -0700 Sender: info-hol-request@ted.cs.uidaho.edu Errors-To: info-hol-request@ted.cs.uidaho.edu Precedence: bulk Received: from swan.cl.cam.ac.uk by ted.cs.uidaho.edu (16.6/1.34) id AA05309; Fri, 30 Apr 93 14:37:28 -0700 Received: from heron.cl.cam.ac.uk (user ww (rfc931)) by swan.cl.cam.ac.uk with SMTP (PP-6.5) to cl; Fri, 30 Apr 1993 09:46:20 +0100 To: info-hol@ted.cs.uidaho.edu Subject: Addition to mweb Date: Fri, 30 Apr 93 09:45:28 +0100 From: Wai Wong Message-Id: <"swan.cl.cam.:221350:930430084632"@cl.cam.ac.uk> A couple of utility programs have been added to the mweb package in the contrib directory in the Cambridge HOL ftp site. The program `winnow' converts a LaTeX file into a master file. The LaTeX file contains segments of HOL/ML codes which are delimited by a pair of macros. These will be put in the code part in the master file generated by winnow. The program `mmerge' merges the output of a HOL session with the input to create a tag file. The Manual has been revised to include document for these programs. A brief description of the implementation of these utilities is added to provide a guide for those who want to modify or extend the program to suit particular applications. Note: mweb can be used with HOL90 without modification. --------------------------------- Wai Wong ww@cl.cam.ac.uk University of Cambridge Computer laboratory New Museums Site Pembroke Street Cambridge CB2 3QG Tel:+44 223 334688 England =========================================================================