[isabelle] proofterm bug?




Hi,

 If you examine line 736 of the output of command

full_prf less_max_iff_disj

you will see

(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.

Best,

Sean

If line numbers are off, just search for
"(thm " with the space.  It's the only one in the output.







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