src/HOL/Analysis/Vitali_Covering_Theorem.thy
changeset 79010 aceca8baf804
parent 73648 1bd3463e30b8
child 79566 f783490c6c99