Re: [isabelle] monadic function definition
As I wrote in my last post, Alex Krauss' paper about partial_function describes it.
Another application can be found in Johannes' and my ITP paper this year:
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and