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

[Gerwin Klein]

The AFP web view doesn't seem to be down from here. The change set is this one, I think:

http://sourceforge.net/p/afp/code/ci/b1e24b9aaa77a61c7b199cdb6f21aaef3492c0c1/

Cheers,
Gerwin

On 25/07/2013, at 9:10, "Florian Haftmann" <florian.haftmann at informatik.tu-muenchen.de<mailto: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

_______________________________________________
isabelle-dev mailing list
isabelle-dev at in.tum.de<mailto:isabelle-dev at in.tum.de>
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

________________________________

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.