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
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
