Universal_Hash_Families and Expander_Graphs: Framework for pseudorandom objects

Pseudorandom objects as a combinator library was formerly incorrectly part of the Distribtued_Distinct_Elements
AFP entry due to chronological reasons. But it belongs conceptually to the Universal_Hash_Families and
Expander_Graphs entries, which this patch accomplishes.

Compared to the former development in DDE the new framework also includes several improvements:

• Constructive implementation of hash families
• An object is always non-empty - this means every object induces naturally a PMF, which removes a lot of constraints from the theorems.

Note: The theory DDE/Pseudorandom_Combinators is now obsolete. I will remove it shortly before the next release
(to minimize the possibility of merge-conflicts).