[isabelle-dev] Abbreviations + Monad_Syntax introduce unit itself additional type variable

2013-09-19 Thread Peter Lammich
Referring to Isabelle_2013 AND Isabelle_12_Sep_2013: In the following example, using an abbreviation that contains monad-syntax introduces a superfluous additional itself-parameter, that, however, is immediately instantiated to unit itself. Note that, when replacing abbreviation by definition,

Re: [isabelle-dev] NEWS: Dockable window Find

2013-09-19 Thread Makarius
On Thu, 19 Sep 2013, Holger Gast wrote: On 09/18/2013 11:07 PM, Makarius wrote: On Wed, 18 Sep 2013, Holger Gast wrote: Well, one more piece of information about Swing gathered. (Not very useful though: like many people nowadays, I have switched to the much faster and more modern SWT/JFace

Re: [isabelle-dev] jedit interface

2013-09-19 Thread Makarius
On Wed, 18 Sep 2013, Tobias Nipkow wrote: I just noticed the following behaviour in 705f0b728b1b: When the cursor remains fixed in the theory window and I scroll in that window with the help of the scoll bar, the output window goes blank when the line with the cursor is no longer visible. I

Re: [isabelle-dev] Clone attacks

2013-09-19 Thread Lawrence Paulson
We also have some overlap between Library/Binomial and Number_Theory/Binomial. --lcp On 19 Sep 2013, at 19:05, Florian Haftmann florian.haftm...@informatik.tu-muenchen.de wrote: Since, there 92080294beb8 are two clone theories: Library/Univ_Poly.thy