Email Gateway (Aug 19 2022 at 14:36): Email Gateway (Aug 19 2022 at 14:36):From: Gergely Buday <gbuday@gmail.com>
Hi,
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.
Email Gateway (Aug 19 2022 at 14:38):From: Makarius <makarius@sketis.net>
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.
Makarius
Email Gateway (Aug 19 2022 at 14:39):From: Buday Gergely <gbuday@karolyrobert.hu>
Makarius wrote:
If the Prover IDE would just externalize and print everything by default,
the front-end would collapse from the mass of the material.
I did not think to print everything in advance. My idea was to show a tooltip that contains the lemma on demand. Clearly ctrl-click takes you to the original proof but this is distracting. I do not see how much burden would this involve but you will tell us.
Last updated: Apr 18 2024 at 16:19 UTC