(* Title: Generat.thy Author: Andreas Lochbihler, ETH Zurich *) section ‹Generative probabilistic values› theory Generat imports Misc_CryptHOL begin subsection ‹Single-step generative›