[isabelle-dev] Fwd: minor generalisation to Imperative_HOL/ex/Imperative_Quicksort, rename Imperative_HOL/ex/Sublist to List_Sublist

These suggestions are worth a discussion. Should we go ahead? Would anybody like to apply this patch and test that everything still works? Larry > Begin forwarded message: > > From: Peter Gammie > Date: 15 November 2015 at 15:15:48 GMT > To:

[isabelle-dev] Future of isatest/afptest

(moving to isabelle-dev) > In the various different isatest configurations for main Isabelle (not > AFP) we do indeed test normal situations, like threads=4 or threads=8, > alongside with abnormal ones like threads=1 or skip_proofs=true. This is definitely something which I will replicate in the

Re: [isabelle-dev] [isabelle] Contracting Abbreviations of Locale Definitions

I have now committed this. See isabelle/e89cfc004f18; the AFP didn't require changes. The final version does not activate abbreviations as aggressively as my first proposal. This was necessary so abbreviations are not propagated over rewrite morphisms, which would have been very confusing.

Re: [isabelle-dev] extra lemmas

These look useful, thanks! I’ll take care of it. Larry Paulson > On 16 Nov 2015, at 16:26, Peter Gammie wrote: > > Can someone add these in at the obvious places? > > thanks, > peter > > lemma LeastI2_wellorder_ex: > assumes "\x::'a::wellorder. P x" > and "\a. \ P a; \b.

[isabelle-dev] popup in ce6320b9ef9b

In more than one example of locale interpretations with "where f = g", where g is a constant, if I hover over the g, the popup shows the type of g twice. Tobias smime.p7s Description: S/MIME Cryptographic Signature ___ isabelle-dev mailing list

Re: [isabelle-dev] Future of permanent_interpretation

Hi Florian, I looked at the documentation generated with this patch, and the first impression of the "Locale interpretation" section is that it now looks funny -- probably due to the transitional nature of the patch. For "interpretation" there are now two declarations and two productions,

Re: [isabelle-dev] minor generalisation to Imperative_HOL/ex/Imperative_Quicksort, rename Imperative_HOL/ex/Sublist to List_Sublist

> On 18.11.2015, at 16:26, Lawrence Paulson wrote: > > These suggestions are worth a discussion. Should we go ahead? Would anybody > like to apply this patch and test that everything still works? I could do it, if nobody has objections. Jasmin