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 20:32:35 +0100
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA20054;
          Thu, 1 Jul 93 12:15:47 -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 AA19949; Thu, 1 Jul 93 12:15:42 -0700
Received: from localhost.cs.ucdavis.edu 
          by toadflax.cs.ucdavis.edu (4.1/UCD.CS.2.3) id AA18517;
          Thu, 1 Jul 93 12:16:03 PDT
Message-Id: <9307011916.AA18517@toadflax.cs.ucdavis.edu>
To: John Harrison <John.Harrison@cl.cam.ac.uk>
Cc: info-hol@ted.cs.uidaho.edu
Subject: Re: proof state on the fly?
In-Reply-To: Your message of "Thu, 01 Jul 93 11:32:30 BST." <"swan.cl.cam.:049080:930701103241"@cl.cam.ac.uk>
Date: Thu, 01 Jul 93 12:16:02 -0700
From: Rob Shaw <shaw@cs.ucdavis.edu>


I see. I just wrap my desired tactic in a \(asl,w), and then
I can set up some let-bindings or whatnot...

Thanx again.

Rob