Re: [isabelle] proof term request



On Mon, 16 Jan 2006, Sean McLaughlin wrote:

>  I mean the latter.  the proof tree is labeled, eg.
> 
> PThm(("induct",_),_,_..)  instead of
> PThm(("Record.product_type.induct",_),...)
> 
> If this is the same in 2005, my request is still open.

It is more or less the same, ignoring the fact that Record.product_type no 
longer exists -- it was used in the record package of Isabelle2004, but 
this is done differently in Isabelle2005 (more efficiently).

As pointed out before, names of closed derivations do not have an 
authentic formal status.  This is a legacy problem in Isabelle, because 
people are used to reuse theorem names at will -- even rebind theorems 
after a theory has been ``finished''.

You should be able to ignore this problem.  Just build your own table of 
closed derivations indexed by the resulting proposition (using structure 
Termtab).  Then you can share proofs of theorems without relying on 
particular naming schemes.


	Makarius





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.