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; Wed, 21 Apr 1993 12:39:32 +0100 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA19734; Wed, 21 Apr 93 04:30:01 -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 AA19729; Wed, 21 Apr 93 04:29:36 -0700 Received: from gadwall.cl.cam.ac.uk (user tl (rfc931)) by swan.cl.cam.ac.uk with SMTP (PP-6.5) to cl; Wed, 21 Apr 1993 12:25:47 +0100 To: info-hol@ted.cs.uidaho.edu Subject: Re: nested subgoals Date: Wed, 21 Apr 93 12:25:36 +0100 From: Laurent Thery Message-Id: <"swan.cl.cam.:283370:930421112606"@cl.cam.ac.uk> ---------------------------- >> 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? That's the kind of issues I've tried to solve with the user-interface I'm currently developed for HOL (which I hope to release soon) For the time being, -- Developing the proof script in the same time than doing the proof is definitevely a good modus operandi (in my interface doing the proof is in fact editing the proof script) -- It's also very useful to have a function that computes diffs between two subgoals. This function can then be applied to give a good feedback about what has changed between the current subgoal and a previous one. --Laurent