src/HOL/Analysis/Embed_Measure.thy
changeset 69678 0f4d4a13dc16
parent 69566 c41954ee87cf
child 69700 7a92cbec7030
equal deleted inserted replaced
69677:a06b204527e6 69678:0f4d4a13dc16