Re: [isabelle] Theorems and types



On Mon, 9 Nov 2015, Mohammad Abdul Aziz wrote:

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?

If you just want to know the types, and not print them explicitly, you can use the C-hover idom of the prover IDE to get a popup with the type information.

This works slightly asymmetrically for input and output of terms, theorems etc.


Here is another possibility to get lots of type information printed (usually way too much):

  declare [[show_types]]
  thm allI
  print_statement allI


	Makarius




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