Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.4) outside ac.uk; Wed, 7 Apr 1993 09:26:57 +0100 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA01400; Wed, 7 Apr 93 01:11:08 -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 AA01393; Wed, 7 Apr 93 01:10:50 -0700 Received: from razorbill.cl.cam.ac.uk (user jg (rfc931)) by swan.cl.cam.ac.uk with SMTP (PP-6.4) to cl; Wed, 7 Apr 1993 09:10:25 +0100 To: info-hol@edu.uidaho.cs.ted Cc: Jim.Grundy@uk.ac.cam.cl Subject: Re: How to STRIP/GEN forall with paired dummy?? Date: Wed, 07 Apr 93 09:10:18 +0100 From: Jim Grundy Message-Id: <"swan.cl.ca.410:07.04.93.08.10.34"@cl.cam.ac.uk> Hmmm, my last message on this got truncated, so here goes again. > Can anyone help me as to how to strip or generalize the following goal: > > "!(p,q,r). p ==> (q==>p)" As John says, just use the pair library: ============================================================================== #load_library `pair`;; Loading library pair ... Extending help search path ................................................................................ ................................................................................ ... pair Library (Revision: 2.1) loaded. Copyright (c) Jim Grundy 1992 Library pair loaded. () : void #g "!(p,q,r:*). p ==> (q==>p)";; "!(p,q,r). p ==> q ==> p" () : void #e PGEN_TAC;; OK.. "p ==> q ==> p" () : void ============================================================================= Note that the version of the pair library releaed with version 2.1 of HOL has a bug in it that will prevent this example working. To get a working version of the pair library you must apply the patch in ftp@cl.cam.ac.uk:hvg/contrib/bugfixes/pair_lib Jim