Re: [isabelle] Reconciling FinFuns in Distro and AFP



Minor clarification:

> This measure is part of a bigger plan to
> a) introduce a type of finite mappings;

This is already ongoing. Johannes and Fabian agreed to replacing the
finite maps in HOL-Probability with a new representation (cf
a4acecf4dc21), which will shortly appear in HOL-Library (it's not high
priority though).

Cheers
Lars




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