Re: [isabelle] Feature suggestion: Replace statement by pretty-printed statement



On Wed, Apr 30, 2014 at 11:54 AM, Tobias Nipkow <nipkow at in.tum.de> wrote:
> Although I do not do this editing that Joachim describes, I also sometimes
> wish that defnitions and lemmas would print the proposition to see what it
> looks like.

I second this. Definitions and the final proof steps of theorem
statements don't have any print output yet, so there's an unused
opportunity to provide information. The final proof steps of have,
show and obtain statements in isar proofs already do this, too.

>
> Tobias
>
> On 30/04/2014 11:16, Joachim Breitner wrote:
>> Dear List,
>>
>> I am currently doing something tedious that I find myself doing often:
>> After having finished a theory I polish it up, including adding nicely
>> looking notation. And then I begin going through my theory, putting the
>> cursor on any lemma declaration or "have" and copy the nicely printed
>> output from the output buffer to the editor buffer.
>>
>> For definitions and "assumes", I first have to call "thm foo_def" or "thm
>> assms" to get hold of that display.
>>
>> It would be great if that process was made easier, maybe by a button in the
>> popup that is (sometimes?) visible when I hover over such a statement, or
>> even better a keyboard combination (similar to how jEdit will format a
>> paragraph when I use "C-e f").
>>
>>
>> Thanks, Joachim
>>
>




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