[isabelle-dev] Proposing extensions to the Isabelle library?
coglio at kestrel.edu
Thu Jul 25 17:44:26 CEST 2013
Hi Florian, thank you for improving and incorporating my changes into Isabelle!
On Jul 25, 2013, at 12:10 AM, Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de> wrote:
> Hi Alessandro,
> see now http://isabelle.in.tum.de/reports/Isabelle/rev/412c9e0381a1
> (unfortunately the corresponding web view for AFP seems down currently –
> but the changeset is therin ;-))
> I adjusted two things:
> * The assumption about Inf is given before the assumption about Sup,
> which is more coherent in the context of the class specification.
> * I have swapped the equation, such that they match existing lemmas.
> PGP available:
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 2095 bytes
Desc: not available
More information about the isabelle-dev