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
> 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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and