[isabelle] Are there more general version of lfp/gfp lemmas with "while" combinator?

 Dear Isabelle users,

Theory While_Combinator proves lemmas for least fixed point (e.g. lfp_while) using finite sets (BTW, the dual versions for gfp are missing for some reason). Are there more general versions of the lemmasÂthat use finite lattices instead?

Alexander Kogtenkov

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