Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Message-Id: <9203100713.AA16050@maui.cs.ucla.edu>
To: info-hol@edu.uidaho.cs.ted
Cc: chou@edu.ucla.cs
Subject: Theorem continuation functions
Date: Mon, 09 Mar 92 23:13:04 PST
From: chou@edu.ucla.cs

I like to use theorem continuation functions to "capture" assumptions.
For instance, suppose I want to prove "A ==> B" for some terms A and B.
Instead of using DISCH_TAC to add A to the set of assumptions and then
worrying about how to get to A again, I would write something like:

(*)     DISCH_THEN (\asm. rest_of_the_proof)

Thus, A is bound to ML identifier asm and can be referred to easily
within rest_of_the_proof as a theorem.  The trouble is that such
tactics are hard to test.  What I usually ended up doing was to
re-run (*) every time I make a refinement to rest_of_the_proof.
Is there a better way?

Any ideas would be appreciated!

- Ching Tsun