Re: [isabelle] monadic function definition
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