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 09:39:33 +0100
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA19340;
          Thu, 1 Jul 93 01:33:09 -0700
Sender: info-hol-request@ted.cs.uidaho.edu
Errors-To: info-hol-request@ted.cs.uidaho.edu
Precedence: bulk
Received: from toadflax.cs.ucdavis.edu by ted.cs.uidaho.edu (16.6/1.34) 
          id AA19335; Thu, 1 Jul 93 01:33:05 -0700
Received: by toadflax.cs.ucdavis.edu (4.1/UCD.CS.2.3) id AA11257;
          Thu, 1 Jul 93 01:33:34 PDT
Date: Thu, 1 Jul 93 01:33:34 PDT
From: shaw@cs.ucdavis.edu (Rob Shaw)
Message-Id: <9307010833.AA11257@toadflax.cs.ucdavis.edu>
To: info-hol@ted.cs.uidaho.edu
Subject: Failure mechanism


Here's a weird one:

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 ]. Yet,

  <tactic1>
 THEN
  DISJ_CASES_TAC thm
 THEN
  FIRST 
  [
    <tactic2>
  ;
    <tactic3>
  ]

proves the goal. To me this looks like THENL is getting involved when
there is not exactly two subgoals, and failing. But how can a successful
DISJ_CASES_TAC not produce exactly two subgoals? Our manuals say this
can't happen. What else can be going on? Not a deeper failure caught
by THENL, because then should the second example above have the same
failure? I'm very confused.

Rob