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

2019-01-31 Thread Mathias Fleury
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

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

2018-09-12 Thread Mathias Fleury
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

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

2017-07-03 Thread Mathias Fleury
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"

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

2017-04-25 Thread Mathias Fleury
ing to the Isabelle repository, I use >> 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 Mathia

Re: [isabelle-dev] macOS Sierra 10.12

2016-10-21 Thread Mathias Fleury
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

Re: [isabelle-dev] Multiset insert

2016-07-27 Thread Mathias Fleury
ermail/isabelle-dev/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 > > &g

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

2016-07-12 Thread Mathias Fleury
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 <mathias.fle...@ens-rennes.fr> wro

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

2016-07-05 Thread Mathias Fleury
board/117/>), 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 <mathias.fle...@ens-rennes.fr> wrote: > > Hi Johannes, > > > the multiset ordering (contrary to the subset orde

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

2016-07-04 Thread Mathias Fleury
e> wrote: > > 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 > > >

[isabelle-dev] Simplification theorems with more general typeclasses

2016-06-28 Thread Mathias Fleury
ld 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 https://m

[isabelle-dev] Lemmas about tranclp and lexn

2015-12-30 Thread Mathias Fleury
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

[isabelle-dev] Isabelle/jEdit - Sidekick

2015-11-10 Thread Mathias Fleury
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

2015-11-10 Thread Mathias Fleury
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] Update of jdk and jedit components

2015-11-04 Thread Mathias Fleury
Thanks for the information, Mathias > On 4 Nov 2015, at 15:55, Makarius <makar...@sketis.net> 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 6d51346

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

2015-11-04 Thread Mathias Fleury
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