[isabelle] Complete Lattices


I have noticed that there is a general theory about complete latices in Isabelle,
however I was not able to use it. I have tried imports CompleteLattices
but it did not work. I tried also imports Lattice CompleteLattices, but
it did not work either.

The second question is how do use these abstract theories? I need
to instantiate them for the lattice of  predicate transformers
('a set => 'a set) with the order inherited from sets (bool).

Best regards,

Viorel Preoteasa

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