Re: [isabelle] Proof_Context abstraction

On Wed, 30 Jul 2014, Peter Lammich wrote:

On Mi, 2014-07-30 at 09:23 +0200, Lars Hupel wrote:
Since you mention type-driven: Do you know of a way of having the
system tell me the types of non-exported functions in existing ML
code in Pure/? The exported functions have their types visible in the
signature specification.

I'm even more low-tech: I have a console open in src/, and use
 grep "val <fun-name>:" -r .
this usually matches the line in the signature that declares the type.

The same could be achieved with jedits (mouse-intensive) hypersearch

Hypersearch is indeed the one big thing of jEdit, independently of the Prover IDE. It is my main tool for navigating the Isabelle bootstrap sources: its uniform naming conventions make this work very well.

The "implementation" manual also explains how Isabelle/ML is usually written, such that it is reasonably easy to read it systematically, with or without tool support.


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