src/HOL/Analysis/Embed_Measure.thy
changeset 63991 0d8cd1f3c26d
parent 63886 685fb01256af
child 67241 73635a5bfa5c