[isabelle-dev] [isabelle] Reconciling FinFuns in Distro and AFP

[Florian Haftmann]

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:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 819 bytes
Desc: OpenPGP digital signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20160920/aa69330c/attachment.asc>