Lars Hupel

2016-09-05 09:00:50 UTC

This measure is part of a bigger plan to

a) introduce a type of finite mappings;

This is already ongoing. Johannes and Fabian agreed to replacing thea) introduce a type of finite mappings;

finite maps in HOL-Probability with a new representation (cf

a4acecf4dc21), which will shortly appear in HOL-Library (it's not high

priority though).

Cheers

Lars