[isabelle] Complete Lattices



Hello,

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.