Re: [isabelle] Knaster-Tarski Lemma

Hi Alfio,

> However, even after importing Lattice_Syntax it is still necessary to
> provide the following
> declaration
> notation
>   less_eq (infix "⊑" 50)
> Its is hidden (via no_notation) at the end of Complete_Lattice and not
> available in Lattice_Syntax.thy

This squared syntax is a special »feature« of Lattices.thy and
Complete_Lattice.thy.  There has been some discussion whether it should
be removed there, but this never evolved into some kind of action.

Hope this helps,


PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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