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; Tue, 20 Apr 1993 21:34:52 +0100
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA17299;
          Tue, 20 Apr 93 13:29:04 -0700
Sender: info-hol-request@ted.cs.uidaho.edu
Errors-To: info-hol-request@ted.cs.uidaho.edu
Precedence: bulk
Received: from panther.cs.uidaho.edu by ted.cs.uidaho.edu (16.6/1.34) 
          id AA17294; Tue, 20 Apr 93 13:29:00 -0700
Received: by panther.cs.uidaho.edu id AA20367 (5.65c/IDA-1.4.4 
          for info-hol@ted); Tue, 20 Apr 1993 13:28:58 -0700
From: Mike Coe <coe@panther.cs.uidaho.edu>
Message-Id: <199304202028.AA20367@panther.cs.uidaho.edu>
Subject: nested subgoals
To: info-hol@ted.cs.uidaho.edu
Date: Tue, 20 Apr 93 13:28:56 PDT
X-Mailer: ELM [version 2.3 PL11]



I am currently doing a very large proof which breaks 
down into several subgoals.  And each one of 
those subgoals breaks down into several 
subgoals and so on.

It has become so bad I can not keep track 
of what conditions brought me to the 
current subgoal.

Is there a way to make HOL tell me
what conditions due to 
BOOL_CASES, ASM_CASES_TAC, or 
STRUCT_CASES_TAC brought me to 
the current subgoal?



thanks, 


mike

Michael L Coe                 |  "A mind is a terrible thing."
Laboratory of Applied Logic   | 
University of Idaho           | 
coe@leopard.cs.uidaho.edu     | 
coe861@snake.cs.uidaho.edu