[isabelle] Theorems and types



Dear all,
I have two questions regarding types of variables in Isabelle theorems:
 1) I understand that a way to print a theorem T in the library is by
printing thm M in the editor. Is there a way to ask for printing the types
of the bound variable?
 2) I understand that to instantiate a quantified variable x in a theorem T
with a term t, one uses T[of "t"]. Is there an equivalent way to
instantiate polymorphic type variables in a theorem?

Best,
Mohammad



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