src/HOL/Analysis/Regularity.thy
changeset 69242 c911716d29bb
parent 69173 38beaaebe736
child 69260 0a9688695a1b