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
This archive was generated by a fusion of
Pipermail (Mailman edition) and