Return-Path: Delivery-Date: Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Sun, 1 Oct 1995 12:52:37 +0100 Received: by leopard.cs.byu.edu (1.37.109.15/16.2) id AA042316865; Sun, 1 Oct 1995 05:27:45 -0600 Sender: info-hol-request@lal.cs.byu.edu Errors-To: info-hol-request@lal.cs.byu.edu Precedence: list Received: from vanuata.dcs.gla.ac.uk by leopard.cs.byu.edu with ESMTP (1.37.109.15/16.2) id AA042286863; Sun, 1 Oct 1995 05:27:43 -0600 Received: from gozo.dcs.gla.ac.uk by vanuata.dcs.gla.ac.uk with LOCAL SMTP (PP); Sun, 1 Oct 1995 12:27:34 +0100 To: info-hol@leopard.cs.byu.edu Cc: tfm@dcs.gla.ac.uk Subject: Training course materials available. Date: Sun, 01 Oct 1995 12:27:31 +0100 From: Tom Melham Message-ID: <"swan.cl.cam.:163660:951001115311"@cl.cam.ac.uk> At the Higher Order Logic Theorem Proving workshop in Utah, I announced the availability of my training materials on the HOL system and its applications. These include OHP transparencies, lecture notes, trainer's notes, and online exercises. There are versions for both HOL88 and HOL90. I am happy to make the course materials available to anyone who wants to use them for training purposes, subject to the conditions that * the materials may not, in part or as a whole, be sold or otherwise distributed for commercial gain, and * acknowledgement is given to the author. If you are interested in a copy, please contact me by email, and I'll arrange for you to get it. You can see the outline of a training course based on these materials by pointing your Web browser at the URL: http://www.dcs.glasgow.ac.uk/~tfm/holcourse.html Tom Melham PS: I am grateful for the support of Rockwell-Collins UK Ltd, who supplied funding to revise and maintain these training materials.