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:

http://www.infsec.ethz.ch/people/andreloc/publications/lochbihler14itp.pdf

Best,
Andreas




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