src/HOL/Analysis/Vitali_Covering_Theorem.thy
changeset 75311 5960bae73afe
parent 73648 1bd3463e30b8
child 79566 f783490c6c99