Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Mon, 14 Jun 1993 16:03:50 +0100 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA08888; Mon, 14 Jun 93 07:52:21 -0700 Sender: info-hol-request@ted.cs.uidaho.edu Errors-To: info-hol-request@ted.cs.uidaho.edu Precedence: bulk Received: from stroma.dcs.ed.ac.uk by ted.cs.uidaho.edu (16.6/1.34) id AA08883; Mon, 14 Jun 93 07:52:01 -0700 Received: from ailsa.dcs.ed.ac.uk by dcs.ed.ac.uk id aa15291; 14 Jun 93 15:49 BST Message-Id: <2992.9306141449@ailsa.dcs.ed.ac.uk> Received: from mjm.localhost.dcs.ed.ac.uk by ailsa.dcs.ed.ac.uk; Mon, 14 Jun 93 15:49:05 +0100 To: info-hol@ted.cs.uidaho.edu Subject: Re: manipulate several subgoals? In-Reply-To: Your message of "Mon, 14 Jun 93 14:45:16 BST." <"swan.cl.cam.:049100:930614134536"@cl.cam.ac.uk> Date: Mon, 14 Jun 93 15:49:03 +0100 From: Matthew Morley The phrase "quick and dirty hack" occurs rather frequently already in this (quite interesting) discussion. I am a little suprised, surely one wants a nice, elegant solution to the problem, hopefully one that is general enough to be useful again and again? So, the elegant solution to the original poster's question should be very much along the lines of what he though MAP_EVERY ought to do -- i.e. map a tactic along a list of subgoals. I am not a hol expert by any means, but my understanding is that in order to do this I will have to write some ML to manipulate the goal stack explicitly, rather than just composing tactics with tacticals. Have such experiments been tried already, in the hol community? M ------------------------------------------------------------------------------ -----Computers are intellectual tools of the last resort" - Thanks Chris!----- ---Matthew Morley, LFCS, Computer Science, Edinburgh University, 1607 JCMB,--- ---The King's Buildings, Mayfield Road, Edinburgh EH9 3JZ. Tel 031 650 5188---