[isabelle-dev] the function "real"

The first phase of this project is finished: the function “real” now has the monomorphic type nat => real and is simply an abbreviation for the generic function, of_nat. In addition, the function “real_of_int” abbreviates the generic function of_int. It took about a week to convert all the

[isabelle-dev] Isabelle/jEdit - Sidekick

Hello list, in the sidekick there is a "sub-panel"^1 below the sidekick (see the red rectangle in the joint screenshot). Is there a way to have line breaks in it? The difference between it and the tooltips that appear in the sidekick, is that the tooltips disappear, when moving the cursor,

Re: [isabelle-dev] NEWS: State panel

Hello Makarius, this might be intended, but in Isabelle/a99125aa964f from this morning the errors and warnings still goes to the output panel, which means that both panel have to be opened at the same time. Could you give us some insights about your workflow (for theorem proving) with the

Re: [isabelle-dev] NEWS: State panel

> On 9 Nov 2015, at 9:41 pm, Makarius wrote: > > * The State panel manages explicit proof state output, with jEdit action > "isabelle.update-state" (shortcut S+ENTER) to trigger update according > to cursor position. > > * The Output panel no longer shows proof state output

Re: [isabelle-dev] NEWS: State panel

Hi Makarius, I noticed some strange behavior: if one triggers state output on the same command but after changing the state, the state output does not change. Consider this example: lemma assumes False shows "False ∧ False" (*using assms*) apply simp If you trigger output on the

Re: [isabelle-dev] NEWS: State panel

On 10/11/2015 14:20, Gerwin Klein wrote: On 9 Nov 2015, at 9:41 pm, Makarius wrote: * The State panel manages explicit proof state output, with jEdit action "isabelle.update-state" (shortcut S+ENTER) to trigger update according to cursor position. * The Output panel no