src/HOL/Analysis/Embed_Measure.thy
changeset 64267 b9a1486e79be
parent 63886 685fb01256af
child 67241 73635a5bfa5c
equal deleted inserted replaced
64265:8eb6365f5916 64267:b9a1486e79be