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?

Use print_statement.

>  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.

  -- Lars




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