Re: [isabelle-dev] Update of jdk and jedit components

Hello Makarius, I am a bit surprised that the content of the tooltips and the output panel can be changed (both in 6d513469f9b2 and Isabelle_23-Oct-2015). Step to reproduce: * open a theory file * type a lemma * select some text of the output panel * type any letter Result: the selected

Re: [isabelle-dev] Update of jdk and jedit components

Thanks for the information, Mathias > On 4 Nov 2015, at 15:55, Makarius wrote: > > On Wed, 4 Nov 2015, Mathias Fleury wrote: > >> I am a bit surprised that the content of the tooltips and the output panel >> can be changed (both in 6d513469f9b2 and Isabelle_23-O

[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, whil

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 ne

[isabelle-dev] Lemmas about tranclp and lexn

Dear list, I stumbled upon some lemmas that have a counterpart in Isabelle (like rtranclp_mono vs tranclp_mono), but are not included. Is there a reason why the following lemmas are not included in Isabelle? rtranclp vs tranclp: there is a rtranclp_mono "r ≤ s ==> r^** ≤ s^**", but no tranclp_

[isabelle-dev] Simplification theorems with more general typeclasses

, would it make sense to use this version in Isabelle? Thanks in advance, Mathias Fleury * for natural numbers, the simproc Numeral_Simprocs.natle_cancel_numerals is able to do it too.___ isabelle-dev mailing list isabelle-...@in.tum.de http

Re: [isabelle-dev] Simplification theorems with more general typeclasses

gt; > Hi Mathias, > > there is at least the type class 'canonically_ordered_monoid' which has > the property a <= b <--> ?c. a + c = b which implies 0 <= a for all a. > Are the multisets already in this typeclass? > > - Johannes > > > Am Dienstag, den

Re: [isabelle-dev] Simplification theorems with more general typeclasses

7/>), and does not need any AFP change. Does someone have an opinion on this change? Mathias > On 04 Jul 2016, at 14:20, Mathias Fleury wrote: > > Hi Johannes, > > > the multiset ordering (contrary to the subset ordering) does not have this > property: &

Re: [isabelle-dev] Simplification theorems with more general typeclasses

For the record, I have now pushed the change to Isabelle, see http://isabelle.in.tum.de/reports/Isabelle/rev/3365c8ec67bd <http://isabelle.in.tum.de/reports/Isabelle/rev/3365c8ec67bd>. Mathias > On 05 Jul 2016, at 14:03, Mathias Fleury wrote: > > Hi all, > > after som

Re: [isabelle-dev] Multiset insert

Hello all, (Relaunching this nearly-one-and-a-half-years-old thread.) Before I start working on it, has anyone already done some work towards adding insert_mset? Thanks, Mathias > On 08 Apr 2015, at 11:12, Larry Paulson wrote: > > Sounds logical to me. > Larry > >> On 8 Apr 2015, at 08:13

Re: [isabelle-dev] Multiset insert

2016-March/006743.html <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/2016-March/006743.html>, but I don't see an explicit conclusion on the best name. I don't remember any other discussion. Mathias > > Tobias > > > On 26/07/2016 13:59, Mathi

Re: [isabelle-dev] macOS Sierra 10.12

Hello Makarius, > Has anybody tried Sierra already? That can be done by the .dmg provided > on http://isabelle.in.tum.de/devel I am using Isabelle devel and RC0 on Sierra (for two weeks), without problem so far. Mathias > The official platform support sche

Re: [isabelle-dev] Uses of Jenkins at TUM

>> the Jenkins testboard installation to see whether something broke. It works >> more reliably than the previous testboard infrastructure, which often >> ignored some commits. > The same applies to me (VU Amsterdam), and I believe Mathias Fleury (MPII > Saarbrücken) is

Re: [isabelle-dev] NEWS: Isabelle/VSCode

Dear Makarius, I am using Isabelle/VSCode code for a week now. So it is possible to install and use it. I mostly like it: * I really like VSCode's Control-P to search for commands. * the PIDE protocol, unlike "isabelle build", accepts unicode characters: If the file contains "×⇩r" inst

Re: [isabelle-dev] AFP dependencies: Refine_Imperative_HOL

Hello all, as a user of the Refinement Framework, there is a key difference between the sessions Sepref_IICF and Refine_Imperative_HOL: the former does not include the tutorial while the latter does. I find it extremely useful to be able to use Sepref_IICF as parent session and still be able to ru

Re: [isabelle-dev] Explorer.thy [was: performance problems]

Hi all, I have my own version of explore (https://bitbucket.org/isafol/isafol/src/master/lib/Explorer.thy ), which does not have better pretty printing, but has two variants that I find indispensable: explore_have produces "have

Re: [isabelle-dev] NEWS: generated code as proper theory export

Hi Makarius, > On 31. Jan 2019, at 20:10, Makarius wrote: > > On 31/01/2019 18:27, Peter Lammich wrote: >> On Do, 2019-01-31 at 16:03 +0100, Makarius wrote: >>> I have looked around at typical uses of 'export_code' in AFP. Most of >>> the time it is just informative: writing a file and looking a