Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) outside ac.uk; Mon, 28 Jun 1993 00:22:34 +0100
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA13778;
          Sun, 27 Jun 93 16:14:25 -0700
Sender: info-hol-request@ted.cs.uidaho.edu
Errors-To: info-hol-request@ted.cs.uidaho.edu
Precedence: bulk
Received: from [192.41.146.1] by ted.cs.uidaho.edu (16.6/1.34) id AA13773;
          Sun, 27 Jun 93 16:14:17 -0700
Received: from pictor.csis.dit.csiro.au by lynx (4.1/1.4S) id AA09972;
          Mon, 28 Jun 93 09:14:34 EST
Received: by pictor.csis.dit.csiro.au (4.1/1.3C) id AA04024;
          Mon, 28 Jun 93 09:14:32 EST
Date: Mon, 28 Jun 93 09:14:32 EST
From: donald@csis.dit.csiro.au
Message-Id: <9306272314.AA04024@pictor.csis.dit.csiro.au>
To: info-hol@ted.cs.uidaho.edu
Subject: Re: smarttacs for HOL90?

> 
> Has anyone ported "smarttacs" to HOL90?  If so, may I have a copy?
> 
> Thanks in advance!
> 

From memory (I daren't go back and look at the code) they could really
do with a proper rewrite - the code developed rather awkwardly as I
realised there were more things I wanted the tactics to do.  I'm out
of the HOL scene for at least a while, but if someone else wants to write them
properly given that what they do is now more or less settled I'd be
glad.

Donald Syme.