Re: [isabelle] monadic function definition

Dear Gergely,

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.
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:


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