Dear Isabelle developers,
this is an update about recent and upcoming changes in the build
infrastructure.
* Starting with Isabelle/e0513d6e4916 and AFP/e6727c33 I have moved
the Jenkins build scripts into the Isabelle and AFP repository (they
used to reside in a private "admin" repository).
On 12/06/2016 18:22, Florian Haftmann wrote:
Thus I would like to understand why we cannot reuse Sup etc in HOLCF
like we do for all the other variants of lattices we have. We would
probably need a suitable type class because at the moment lub is
unrestricted.
For each type class, per type co
> Thus I would like to understand why we cannot reuse Sup etc in HOLCF
> like we do for all the other variants of lattices we have. We would
> probably need a suitable type class because at the moment lub is
> unrestricted.
For each type class, per type constructor there is at most *one*
instance.
On 11/06/2016 21:26, Florian Haftmann wrote:
For the moment I think bold syntax in the first choice. In the middle
run I would suggest to have a closer look at HOLCF/Porder.thy to see
whether something can be done to integrate it more with the standard
type classes; a least it formalizes a lot
