Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.2); Tue, 13 Oct 1992 18:50:29 +0100 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA20513; Tue, 13 Oct 92 10:34:58 -0700 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Precedence: bulk Received: from Sun.COM by ted.cs.uidaho.edu (16.6/1.34) id AA20507; Tue, 13 Oct 92 10:34:52 -0700 Received: from Eng.Sun.COM (zigzag-bb.Corp.Sun.COM) by Sun.COM (4.1/SMI-4.1) id AA13981; Tue, 13 Oct 92 10:34:00 PDT Received: from lara.Eng.Sun.COM by Eng.Sun.COM (4.1/SMI-4.1) id AA05424; Tue, 13 Oct 92 10:34:02 PDT Received: by lara.Eng.Sun.COM (4.1/SMI-4.1) id AA00266; Tue, 13 Oct 92 10:35:42 PDT Date: Tue, 13 Oct 92 10:35:42 PDT From: Paul.Loewenstein@COM.Sun.Eng (Paul Loewenstein) Message-Id: <9210131735.AA00266@lara.Eng.Sun.COM> To: info-hol@edu.uidaho.cs.ted In-Reply-To: Tom Melham's message of Tue, 13 Oct 92 17:19:53 +0100 <"swan.cl.ca.458:13.09.92.16.21.46"@cl.cam.ac.uk> Subject: Simple question > > Is there a one-line, standard-stuff-only tactic for changing the goal > > x to the goal F and introducing ~x as a new assumption? I'll be very > > surprised if the answer isn't yes, but I'm tired of trying to figure > > it out from the manual. Will one of you guys who knows the answer > > tell it to me? > > Rewrite once with |- !t. t = ~~t then STRIP_TAC: > > PURE_ONCE_REWRITE_TAC [GSYM(CONJUNCT1 (NOT_CLAUSES))] THEN STRIP_TAC > > where GSYM is defined in version 2.01 by > > let GSYM = CONV_RULE(ONCE_DEPTH_CONV SYM_CONV);; > This is a more elegant custom tactic which does that. let CCONTR_TAC (asl, w) = ([mk_neg w . asl, "F"], (\[th]. CCONTR w th));; Paul Loewenstein -- paul.loewenstein@Eng.sun.com Staff Engineer, Sun Microsystems