Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.2); Tue, 15 Dec 1992 19:25:09 +0000 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA15000; Tue, 15 Dec 92 11:09:59 -0800 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Precedence: bulk Received: from atc.boeing.com by ted.cs.uidaho.edu (16.6/1.34) id AA14995; Tue, 15 Dec 92 11:09:53 -0800 Received: by atc.boeing.com (5.57) id AA03529; Tue, 15 Dec 92 11:06:55 -0800 Received: by elvis.ds.boeing.com (4.1/SMI-4.1) id AA05635; Tue, 15 Dec 92 11:07:40 PST Date: Tue, 15 Dec 92 11:07:40 PST From: dfura@com.boeing.ds.elvis (David Fura) Message-Id: <9212151907.AA05635@elvis.ds.boeing.com> To: info-hol@edu.uidaho.cs.ted Subject: HELP: deleting assumptions Wishnu writes: > Sometimes tactics such as resolutions generate too many assumption, > and one may wish to eliminate those which are really superflous. Is > there any standard tactic that can do this? I have search in manual > but found nothing so far. Did I miss something? I too have found this to be a serious problem and have hacked together the following (simple but not very elegant) tactic. You have to be careful with it since it throws out *all* implicative assumptions. Maybe someone has a more precise solution? let NO_IMP_ASSUME_TAC thm :tactic = \(asl,w). if is_imp(snd(dest_thm thm)) then ALL_TAC (asl,w) else ASSUME_TAC thm (asl,w);; e (POP_ASSUM_LIST (MAP_EVERY (\thm. NO_IMP_ASSUME_TAC thm)));; Dave Fura (dfura@elvis.boeing.com)