[isabelle] display of types

Randy Pollack wrote:

Even though I have "show sorts" on, [] is not shown with a type, but

I've also noticed this - presumably the thinking is, that if a user has declared a constant, he/she knows what type it is.

But often I've found it would be helpful, when a polymorphic constant is used monomorphically (or with a less general polymorphic type) in a theorem, it would be nice to be able to see the type.

Apart from printing out the term (which can give rather long output) is there any way of doing this?


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