Re: [isabelle] monadic function definition



Christian Sternagel wrote:

> And maybe obvious, but I'll say it anyway: "partial_function" and
> do-notation are completely orthogonal.

Now it is obvious :-)

Where can I find some description of the partial_function definition
mechanism? There is a page in the Isar reference manual but that is
not very much detailed.

- Gergely




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