[isabelle-dev] Proposing extensions to the Isabelle library?

[Alessandro Coglio]

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.
> 
> Cheers,
> 	Florian
> 
> -- 
> 
> PGP available:
> http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
> 

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 2095 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20130725/0a0ae09e/attachment.bin>