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.

Indeed.

> 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.

OK.

	Florian

-- 

Home:
http://www.in.tum.de/~haftmann

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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