Re: [isabelle] proof term request



On Sun, 15 Jan 2006, Sean McLaughlin wrote:

> I have a request to modify the proof terms from locales slightly.  
> Right now, theorems which are proved in a locale setting, eg. 
> Record.thy, only label the Thm parts of the proof tree with the short 
> name of the theorem, eg. "induct", when this is suppose to signify 
> "Record.product_type.induct".

Note that "Record.product_type.induct" is used for the exported version of 
that fact.

Anyway, internal theorem names are little more than comments, providing 
some hints about the context where the fact had been derived.  All you can 
do at the moment is to unfold the derivation to get the actual proof term. 
At some point we might establish a clear one-to-one correspondence of 
theorem identifiers and (closed) derivations, but this will probably be 
something like "induct4711".


	Makarius





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