Re: [isabelle] proofterm bug?

Sean McLaughlin wrote:

(thm \cdot TYPE ...

normally theorem applications are labeled by name
eg. thm.HOL.impI

This theorem seems to be unnamed, and is a mystery to me.

Hello Sean,

such unnamed theorems usually appear when intermediate results
in packages (like the datatype package) or simplification procedures
are proved via prove_goalw_cterm (now replaced by Goal.prove in the
development version) and similar functions. Since these theorems are
not stored in the theorem database, they do not get a name.
To unfold such unnamed theorems in a proof term, you can apply the

  Reconstruct.expand_proof <theory> [("", NONE)] <proof>

to it.


Dr. Stefan Berghofer               E-Mail: berghofe at
Institut fuer Informatik           Phone: +49 89 289 17328
Technische Universitaet Muenchen   Fax:   +49 89 289 17307
Boltzmannstr. 3                    Room: 01.11.059
85748 Garching, GERMANY  

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