src/HOL/Analysis/Lebesgue_Integral_Substitution.thy
changeset 69608 2b3a247889f8
parent 69517 dc20f278e8f3
child 69712 dc85b5b3a532