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
Note that "Record.product_type.induct" is used for the exported version of
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".
This archive was generated by a fusion of
Pipermail (Mailman edition) and