Return-Path: <john.harrison-request@uk.ac.cam.cl>
Delivery-Date: 
Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.2);
          Tue, 13 Oct 1992 17:43:08 +0100
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA20329;
          Tue, 13 Oct 92 09:23:30 -0700
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
Received: from swan.cl.cam.ac.uk by ted.cs.uidaho.edu (16.6/1.34) id AA20324;
          Tue, 13 Oct 92 09:23:23 -0700
Received: from scaup.cl.cam.ac.uk (user tfm) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.2) to cl; Tue, 13 Oct 1992 17:20:21 +0100
To: shb@com.oracorp
Cc: info-hol@edu.uidaho.cs.ted, Tom.Melham@uk.ac.cam.cl
Subject: Re: Simple question
In-Reply-To: Your message of Tue, 13 Oct 92 11:42:16 -0400. <9210131542.AA01572@sparta.oracorp.com>
Date: Tue, 13 Oct 92 17:19:53 +0100
From: Tom Melham <Tom.Melham@uk.ac.cam.cl>
Message-Id: <"swan.cl.ca.458:13.09.92.16.21.46"@cl.cam.ac.uk>


> 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);;

Tom