Return-Path: Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.0) id <05646-0@swan.cl.cam.ac.uk>; Thu, 7 May 1992 20:36:19 +0100 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA13201; Thu, 7 May 92 12:14:21 -0700 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Received: from swan.cl.cam.ac.uk by ted.cs.uidaho.edu (16.6/1.34) id AA13195; Thu, 7 May 92 12:14:01 -0700 Received: from guillemot.cl.cam.ac.uk by swan.cl.cam.ac.uk with SMTP (PP-6.0) to cl id <05418-0@swan.cl.cam.ac.uk>; Thu, 7 May 1992 20:13:32 +0100 To: jimaf@edu.uidaho.cs.leopard (Jim Alves-Foss) Cc: info-hol@edu.uidaho.cs.ted Subject: Re: Labeling assumptions in the asl In-Reply-To: Your message of Thu, 07 May 92 10:39:07 -0700. <9205071739.AA19108@leopard.cs.uidaho.edu> Date: Thu, 07 May 92 20:13:29 +0100 From: Tom Melham Message-Id: <"swan.cl.ca.420:07.04.92.19.13.35"@cl.cam.ac.uk> jimaf@edu.uidaho.cs.leopard (Jim Alves-Foss) writes: > I am trying to find a way to intuitively do proofs without using "el" for > explicit assumption numbers. I recall the thread here earlier discussing > several ways of doing that. I have another idea that I don't recall seeing > and wonder if anyone has worked on it. The idea is as follows: > > 1. When you add assumptions to the asl give them a label ("name"): > > ... etc ... > > Any comments would be appreciated. I recall Inder Dhingra (isd@cl.cam.ac.uk) doing something along these lines. Alas, a quick scan of the HOL area does not turn up his code. But I seem to recall that he had to redefine the notion of a tactic. You might ask him about it. Tom