Re: [isabelle] looking up a lemma in Isabelle/JEdit

On Thu, 19 Jun 2014, Gergely Buday wrote:

if there is a reference in a proof to an automatically verified lemma, I can CTRL-click on the name and Isabelle/JEdit takes me to the definition of e.g. the datatype. But the lemma is not explicit there.

Is there a way to display the lemma other than using the Find feature? It would be nice to have a button to display the theorem in a tooltip.

The commands 'thm' or 'print_statement' do that, when put in the proper place in the source, with the proper names of the facts.

If the Prover IDE would just externalize and print everything by default, the front-end would collapse from the mass of the material. People have already complained that underpowered hardware is overloaded by the default setup of Isabelle/jEdit, which produces more than an order of magnitude more content than was done in the past.

Extremely light machines are fashionable, but another reason for the trend is the unability of most software applications to make use of big machines today, which means many cores. This does not mean that Isabelle defaults will become airy, but stay in somewhere in the middle: high-end laptops or midrange workstations.


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