[isabelle] mutual primrecs



A while back, Tobias suggested that better support for mutually
recursive function definitions was in the pipeline.  It would be
useful to know when we might hope for them, if there are any concrete
plans for them in a near-term release?  (so that we could avoid
embarking on tupling or higher-order encodings, eg for primrecs of n*m
mutually recursive functions, n each over m mutually recursive datatypes).

many thanks,
Peter





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