Re: [isabelle] Reconciling FinFuns in Distro and AFP

> 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).

See now Isabelle/2359e9952641. This contains some initial code setup
which should be enough for most purposes; it uses "AList" underneath.

There is a prime candidate for consolidation in the AFP (see
"Finite_Map2" theory), which I attempted to port, but then "back"ed out
(literally â there is a proof with over 10 "back" statements which I
would've had to fix). In case anyone is particularly adventurous, feel
free to go ahead ...


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