src/HOL/Analysis/Embed_Measure.thy
changeset 69710 61372780515b
parent 69700 7a92cbec7030
child 69768 7e4966eaf781