Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.2); Thu, 3 Dec 1992 13:30:39 +0000 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA20469; Thu, 3 Dec 92 04:59:39 -0800 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Precedence: bulk Received: from ganymede.inmos.co.uk by ted.cs.uidaho.edu (16.6/1.34) id AA20464; Thu, 3 Dec 92 04:59:31 -0800 Received: from frogland.inmos.co.uk by ganymede.inmos.co.uk; Thu, 3 Dec 92 12:58:55 GMT From: David Shepherd Message-Id: <23736.9212031259@frogland.inmos.co.uk> Subject: Re: HELP: RES_TAC To: wishnu@nl.ruu.cs (Wishnu Prasetya) Date: Thu, 3 Dec 1992 12:59:15 +0000 (GMT) Cc: info-hol@edu.uidaho.cs.ted In-Reply-To: <199212031241.AA01381@infix.cs.ruu.nl> from "Wishnu Prasetya" at Dec 3, 92 01:41:45 pm X-Mailer: ELM [version 2.4 PL3] Content-Type: text Content-Length: 969 Wishnu Prasetya has said: > > Hi there! > > Just a small question. Any idea why RES_TAC does not create any new assumption > in the case below? I would say it should. > > OK.. > "WELL_FOUNDED(R 0)" > [ "0 < n \/ (0 = n) ==> WELL_FOUNDED(R 0)" ] > [ "0 < n \/ (0 = n)" ] > > () : void > > #e RES_TAC;; > OK.. > "WELL_FOUNDED(R 0)" > [ "0 < n \/ (0 = n) ==> WELL_FOUNDED(R 0)" ] > [ "0 < n \/ (0 = n)" ] > > () : void in the preparation stage for resolution RES_TAC turns the implication into ["0 < n ==> WELL_FOUNDED(R 0)"; "0 = n ==> WELL_FOUNDED(R 0)"] POP_ASSUM STRIP_ASSUME_TAC THEN RES_TAC would work. -------------------------------------------------------------------------- david shepherd: des@inmos.co.uk or des@inmos.com tel: 0454-616616 x 625 inmos ltd, 1000 aztec west, almondsbury, bristol, bs12 4sq 1992: celebrate the quincentenary of columbus getting lost