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

Gerwin Klein Gerwin.Klein at nicta.com.au
Thu Jul 25 11:20:58 CEST 2013

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



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.



PGP available:

isabelle-dev mailing list
isabelle-dev at in.tum.de<mailto:isabelle-dev at in.tum.de>


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.

More information about the isabelle-dev mailing list