src/HOL/Analysis/Regularity.thy
changeset 74971 16eaa56f69f7
parent 74362 0135a0c77b64