Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) outside ac.uk; Thu, 1 Jul 1993 11:55:09 +0100
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA19389;
          Thu, 1 Jul 93 03:43:35 -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 AA19384;
          Thu, 1 Jul 93 03:43:29 -0700
Received: from auk.cl.cam.ac.uk (user jrh (rfc931)) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) to cl; Thu, 1 Jul 1993 11:43:18 +0100
To: shaw@cs.ucdavis.edu (Rob Shaw)
Cc: info-hol@ted.cs.uidaho.edu
Subject: Re: Failure mechanism
In-Reply-To: Your message of "Thu, 01 Jul 93 01:33:34 PDT." <9307010833.AA11257@toadflax.cs.ucdavis.edu>
Date: Thu, 01 Jul 93 11:43:08 +0100
From: John Harrison <John.Harrison@cl.cam.ac.uk>
Message-Id: <"swan.cl.cam.:051410:930701104334"@cl.cam.ac.uk>


Rob Shaw writes:

> The following tactic:
> 
>   <tactic1>
>  THEN
>   DISJ_CASES_TAC thm
>  THENL
>   [
>     <tactic2>
>   ;
>     <tactic3>
>   ]
> 
> fails with THENL, even when both <tactic2> and <tactic3> have the form
> FIRST [ ..... ; ALL_TAC ].

I am not sure if this is your problem, but the following caught me several
times early on in my use of HOL.

Suppose for concreteness that |tac1| and |tac2| both split their goal into
two subgoals, and you want to apply |tac2| followed by two other tactics to
each of the subgoals from |tac1|. Then

  tac1 THEN tac2 THENL [....; ....]

will not work because the THEN(L)s associate to the left; you need

  tac1 THEN (tac2 THENL [....; ....])

In other words, your problem would be explicable if your tactic <tactic1>
generated multiple subgoals, and could be solved by bracketing.

John.