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 10:27:57 +0000 Received: by leopard.cs.byu.edu (1.37.109.7/16.2) id AA06519; Fri, 19 Nov 93 03:11:52 -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 AA06515; Fri, 19 Nov 93 03:11:40 -0700 Received: from ux7.tfl.dk by dworshak.cs.uidaho.edu with SMTP (1.37.109.4/16.2) id AA24847; Fri, 19 Nov 93 02:09:40 -0800 Received: by ux7.tdr.dk (/\==/\ Smail3.1.24.1 #24.1) id ; Fri, 19 Nov 93 11:09 MET Message-Id: Date: Fri, 19 Nov 93 11:09 MET From: kimdam@tdr.dk (Kim Dam Petersen) To: info-hol@cs.uidaho.edu Subject: Is there an OK_TAC 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. Regards, Kim Dam Petersen