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
isab
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. P b \ a \ b
> \ \
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@mailbroy.informatik.tu-muenchen.de
> Su
(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
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.
I
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, whil
> 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
___