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; Sun, 25 Apr 1993 02:01:58 +0100
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA00042;
          Sat, 24 Apr 93 11:12:38 -0700
Sender: info-hol-request@ted.cs.uidaho.edu
Errors-To: info-hol-request@ted.cs.uidaho.edu
Precedence: bulk
Received: from Baleen.CS.UCLA.EDU by ted.cs.uidaho.edu (16.6/1.34) id AA00037;
          Sat, 24 Apr 93 11:12:33 -0700
Received: by makaha.cs.ucla.edu (Sendmail 5.61a+YP/2.27) id AA29531;
          Sat, 24 Apr 93 11:12:31 -0700
Date: Sat, 24 Apr 93 11:12:31 -0700
From: toal@CS.UCLA.EDU (Ray J. Toal)
Message-Id: <9304241812.AA29531@makaha.cs.ucla.edu>
To: markaa@ee.cornell.edu
Subject: Re: smarttacs
Cc: info-hol@ted.cs.uidaho.edu

I use REPEATED_SMART_EXISTS_TAC all the time, with pretty good results.
BUT, sometimes it is too heavy handed, and it tends to miss eliminating
an existentially quantified variable that appears in more than one
conjunct.  Also, I've found that using RENAME_TAC before this tactic
is often necessary.  A good alternative to this tactic is
the conversion REDUCE in the ind_defs library.

Ray Toal