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,
	Florian

-- 

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.