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