See now #55256a98f65f.

The proofs are really a challenge…

Am 16.09.2016 um 22:29 schrieb Lars Hupel:
>> 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 ...
> Cheers
> Lars


PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

isabelle-dev mailing list

Reply via email to