src/HOL/Analysis/Embed_Measure.thy
changeset 69109 c9ea9290880f
parent 67399 eab6ce8368fa
child 69180 922833cc6839
equal deleted inserted replaced
69024:287bb00371c1 69109:c9ea9290880f