Re: [isabelle] monadic function definition

Dear Gergely,

there also is the AFP-entry Partial-Function-MR which allows you to define
sets of mutual recursive partial functions (which is not possible using the 
original partial-function command). In the entry you also find further 
examples of partial functions, including Collatz and a potentially 
non-terminating evaluator for (a kind of) mu-recursive expressions.


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