[isabelle] proofterm bug?


 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.



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.