(* Title: Generative_Probabilistic_Value.thy Author: Andreas Lochbihler, ETH Zurich *) theory Generative_Probabilistic_Value imports Resumption Generat "HOL-Types_To_Sets.Types_To_Sets" begin hide_const (open) Done subsection ‹Type definition› context notes [[bnf_internals]] begin