Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.4) outside ac.uk; Thu, 28 Jan 1993 17:25:07 +0000 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA13296; Thu, 28 Jan 93 09:11:19 -0800 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Precedence: bulk Received: from relay.pipex.net by ted.cs.uidaho.edu (16.6/1.34) id AA13290; Thu, 28 Jan 93 09:11:02 -0800 X400-Received: by mta relay.pipex.net in /PRMD=pipex/ADMD=cwmail/C=GB/; Relayed; Thu, 28 Jan 1993 17:08:10 +0000 X400-Received: by /PRMD=icl/ADMD=gold 400/C=GB/; converted (ia5 text (2)); Relayed; Thu, 28 Jan 1993 17:05:46 +0000 Date: Thu, 28 Jan 1993 17:05:46 +0000 X400-Originator: R.B.Jones@uk.co.icl.wins.win0109 X400-Recipients: info-hol@edu.uidaho.cs.ted X400-Mts-Identifier: [/PRMD=icl/ADMD=gold 400/C=GB/;win0109 0000012600002218] Original-Encoded-Information-Types: undefined (0) X400-Content-Type: P2-1984 (2) Content-Identifier: 2218 From: R.B.Jones@uk.co.icl.wins.win0109 Message-Id: <"2218*/I=RB/S=Jones/OU=win0109/O=icl/PRMD=icl/ADMD=gold 400/C=GB/"@MHS> To: info-hol@edu.uidaho.cs.ted Subject: ML literate scripts in ProofPower >I gather from a report by International Computers Ltd. that there exist >literate-programming tools -- web, tangle, weave -- for SML. Are any >such tools publicly available? Are there similar publicly available >tools for HOL88 ML? > >Steve Brackin >ORA The ICL ProofPower system is implemented using "literate ML scripts" (and also literate HOL scripts, and Z scripts, and BNF scripts, and C scripts, and Makefile scripts....). The printing of these is done using LaTeX, but no use is made of web, tangle or weave. These facilities would work for HOL88 ML also (and previous versions were used on all our HOL88 work before we switched to ProofPower). The machinery for doing this is supplied with ProofPower. We also were intending to make this more generally available in the public domain, but havn't yet got round to doing so. One advantage of our system is that languages like Z and HOL are supported using an extended font, with spaces, tabs and newlines having their normal significance when printing (this makes the LaTeX source texts legible, almost wysiwyg, for the formal inserts). Roger Jones International Computers Limited R.B.Jones@win0109.wins.icl.co.uk