Re: [isabelle] Theorems and types
On 09.11.2015 17:59, Mohammad Abdul Aziz wrote:
> 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?
You can use [where 'a=T] or [of x for x :: 'a]. However, this should be
very seldom necessary.
This archive was generated by a fusion of
Pipermail (Mailman edition) and