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; Fri, 19 Nov 1993 11:01:50 +0000 Received: by leopard.cs.byu.edu (1.37.109.7/16.2) id AA06620; Fri, 19 Nov 93 03:47:05 -0700 Sender: info-hol-request@leopard.cs.byu.edu Errors-To: info-hol-request@leopard.cs.byu.edu Precedence: bulk Received: from dworshak.cs.uidaho.edu by leopard.cs.byu.edu with SMTP (1.37.109.7/16.2) id AA06616; Fri, 19 Nov 93 03:47:04 -0700 Received: from ganymede.inmos.co.uk by dworshak.cs.uidaho.edu with SMTP (1.37.109.4/16.2) id AA25111; Fri, 19 Nov 93 02:45:01 -0800 Received: from frogland.inmos.co.uk by ganymede.inmos.co.uk; Fri, 19 Nov 1993 10:44:51 GMT From: David Shepherd Message-Id: <23112.9311191044@frogland.inmos.co.uk> Subject: Re: Is there an OK_TAC To: info-hol@cs.uidaho.edu (info-hol mailing list) Date: Fri, 19 Nov 1993 10:44:00 +0000 (GMT) In-Reply-To: from "Kim Dam Petersen" at Nov 19, 93 11:09:00 am X-Mailer: ELM [version 2.4 PL20] Content-Type: text Content-Length: 679 Kim Dam Petersen has said: > > Dear HOL'ers, > > Does HOL support an OK_TAC, i.e. a tactic that solves a goal of form: > > a u A ?- a > ========== OK_TAC > - > > I know that ASM_REWRITE_TAC[] and ACCEPT_TAC(ASSUME a) will do the > trick; I'd just like to know if there is a simple single-named tactic > that solves the problem. val OK_TAC = FIRST_ASSUM ACCEPT_TAC; -------------------------------------------------------------------------- david shepherd: des@inmos.co.uk tel: 0454-616616 x 625 inmos ltd, 1000 aztec west, almondsbury, bristol, bs12 4sq "you might think that --- I couldn't possibly comment"