Re: [isabelle] Problem with unfolding definitions while instantiating class

> This is not possible. As Dave pointed out, the problem goes away if in Main the
> instantiation of "fun" on class complete_lattice is done in stages, where in a
> first step one merely instantiates Sup and Inf.
> @ Florian: any objections to that?

No.  This would finally conclude the »syntactification« of Sup and Inf
initiated by Larry (AFAIR).



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.