[isabelle] How to check type information in Isabelle/ML



Dear Isabelle experts,

I was wondering if there is an easy way to jump to the file where a type in Isabelle/ML is defined. For example, from

  ML {*
  Object_Logic.atomize
  *}

we can know that the function Object_Logic.atomize is of type

  val it = fn: Proof.context -> conv

we can also jump to the definition file of Object_Logic.atomize by CTRL+left click at the method name. However, what if I want to know more about the type "conv", is there a quick way to jump to the file where "conv" is declared or defined? An ideal way might be to CTRL+left click at "conv", but it does not seem to work for now.

Many thanks,
Wenda

--
Wenda Li
PhD Candidate
Computer Laboratory
University of Cambridge




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