[isabelle] Theorems and types
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?
This archive was generated by a fusion of
Pipermail (Mailman edition) and