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 10:18:26 +0100 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA08729; Mon, 14 Jun 93 02:07:18 -0700 Sender: info-hol-request@ted.cs.uidaho.edu Errors-To: info-hol-request@ted.cs.uidaho.edu Precedence: bulk Received: from swan.cl.cam.ac.uk by ted.cs.uidaho.edu (16.6/1.34) id AA08724; Mon, 14 Jun 93 02:07:10 -0700 Received: from heron.cl.cam.ac.uk (user ww (rfc931)) by swan.cl.cam.ac.uk with SMTP (PP-6.5) to cl; Mon, 14 Jun 1993 10:07:10 +0100 To: shaw@cs.ucdavis.edu (Rob Shaw) Cc: info-hol@ted.cs.uidaho.edu, Wai.Wong@cl.cam.ac.uk Subject: Re: manipulate several subgoals? In-Reply-To: Your message of "Sun, 13 Jun 93 20:37:32 PDT." <9306140337.AA23785@toadflax.cs.ucdavis.edu> Date: Mon, 14 Jun 93 10:07:04 +0100 From: Wai Wong Message-Id: <"swan.cl.cam.:295650:930614090716"@cl.cam.ac.uk> If a tactic tac generates n subgoals and you want to do the same thing, say tac2, to all of them, you can said: tac THEN tac2 If you want to do different thing to each of them, you can said: tac THENL [ tac1; tac2;...] If you want to do the same thing, say tac2, to most of them, and tac2 will fail when applied to the remaining subgoals, then you can say: tac THEN (TRY tac2) THEN ... Wai