Return-Path:
Return-Path: <john.harrison-request@uk.ac.cam.cl>
Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.0)
          id <22428-0@swan.cl.cam.ac.uk>; Mon, 9 Mar 1992 19:41:45 +0000
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA29915;
          Mon, 9 Mar 92 11:17:13 -0800
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Received: from scylla.oracorp.com by ted.cs.uidaho.edu (16.6/1.34) id AA29804;
          Mon, 9 Mar 92 11:17:00 -0800
Received: from sparta.oracorp.com by oracorp.com (4.1/2.1-ORA Corporation)
          id AA23731; Mon, 9 Mar 92 14:18:16 EST
Date: Mon, 9 Mar 92 14:18:13 EST
From: shb@com.oracorp
Received: by sparta.oracorp.com (4.1/1.3-ORA Corporation) id AA07706;
          Mon, 9 Mar 92 14:18:13 EST
Message-Id: <9203091918.AA07706@sparta.oracorp.com>
To: info-hol@edu.uidaho.cs.ted
Subject: "Succeeds" predicate?

I'd like a function I could apply to a tactic applied to each of a
number of sugoals with THEN that would cause the tactic to have no
effect on a subgoal unless it succeeded in proving that subgoal.  (I
was recently burned by a tactic that succeeded in proving a number of
subgoals, but transformed one of them so that I didn't recognize it.)
Such a function would be analogous to TRY, but would check for whatever
gives rise to a "subgoal proved" message.  Is there such a thing?  Is
it reasonably easy to write?  I thought I remembered seeing such a
thing in the HOL reference manual, but that now seems to be a case of
wishful/creative memory.

Steve Brackin
ORA Corporation
Ithaca, NY