[isabelle] Complete Lattices
I have noticed that there is a general theory about complete latices in
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).
This archive was generated by a fusion of
Pipermail (Mailman edition) and