Re: [isabelle] Indexed Sum/Product Operator



Am 04/12/2012 12:11, schrieb Makarius:
> That is indeed the way and it is not just by luck, because that is an important
> principle of the Prover IDE: what you see as formally checked source is
> annotated by aspects of the logical content from the prover. So you can explore
> it via tooltips or hyperlinks right in the text.
> 
> Sometimes these "aspects" are still missing or only approximative, but the
> coverage is increasing over time. So the need for separate diagnostic commands
> like find_consts is more and more diminished.

The interesting part of the functionality of find_consts is search by a given
type (a bit like Hoogle, if you speak Haskell). How do you plan to replace that
by tooltips and hyperlinks?

Tobias





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