Re: [isabelle] Lattices and syntactic classes

>>> By declaring your customary class introduction rules Pure.intro, they
>>> are preferred in instance proofs.
>> Does that solve the issues that were raised on this thread earlier?
> To me this looks rather like a workaround for some specific situations.
> If I understand correctly, it wouldn't work with a more complex class
> hierarchy, where parts of the instance may already be established etc.
> The issue certainly deserves more thourough examination at some point.


> For now I have just added (5e51075cbd97) the syntactic classes for inf
> and sup, which were originally asked for by Viorel. This is a rather
> straightforward thing, and the more general typings that may arise seem
> to have little impact in practice.





PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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