Return-Path: Return-Path: Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP) id <28454-0@swan.cl.cam.ac.uk>; Mon, 19 Aug 1991 11:41:55 +0100 Received: from relay2.UU.NET by ted.cs.uidaho.edu (15.11/1.34) id AA22407; Mon, 19 Aug 91 03:34:32 pdt Received: from uunet.uu.net (via LOCALHOST.UU.NET) by relay2.UU.NET with SMTP (5.61/UUNET-internet-primary) id AB25894; Mon, 19 Aug 91 06:35:05 -0400 Received: from inmos-c.UUCP by uunet.uu.net with UUCP/RMAIL (queueing-rmail) id 063430.18321; Mon, 19 Aug 1991 06:34:30 EDT Received: from brwbf.inmos.co.uk by inmos-c.inmos.com with DNI-MTP [1.1] id brwbf-15737; Mon, 19 Aug 91 06:26:21 MDT Received: from ganymede.inmos.co.uk by brwbf.inmos.co.uk; Mon, 19 Aug 91 11:33:10 BST Received: from frogland.inmos.co.uk by ganymede.inmos.co.uk; Mon, 19 Aug 91 11:33:05 BST From: David Shepherd Message-Id: <10537.9108191033@frogland.inmos.co.uk> Subject: user interface changes to HOL To: info-hol@edu.uidaho.cs.ted (info-hol mailing list) Date: Mon, 19 Aug 91 11:32:59 BST X-Mailer: ELM [version 2.3 PL11] schubert@iris.eecs.ucdavis.edu has said: > Printing assumption list numbers: > Though it's bad practice to frequently use (el ? asl), often its the > quickest and easiest way to accomplish some purpose. having come unstuck with this in the move from v11 to v12 (assumption lists changed :-) i now use the following tactic let EXTRACT_ASSUM_THEN ttac t = UNDISCH_TAC t THEN DISCH_TAC THEN POP_ASSUM ttac;; i.e. it extracts assumption t from the assumption list and feeds it to theorem tactic ttac. e.g. EXTRACT_ASSUM_THEN (ASSUME_TAC o SYM) "0=n";; would take an assumption "0=n" out of thr list and then assume "n=0". -------------------------------------------------------------------------- david shepherd: des@inmos.co.uk or des@inmos.com tel: 0454-616616 x 379 inmos ltd, 1000 aztec west, almondsbury, bristol, bs12 4sq "pugh, pugh, barney mcgrew, cuthbert, dibble, grubb !"