[isabelle-dev] [isabelle] Reconciling FinFuns in Distro and AFP
florian.haftmann at informatik.tu-muenchen.de
Tue Sep 20 10:29:29 CEST 2016
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 ...
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 819 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev