src/HOL/Analysis/Regularity.thy
changeset 78517 28c1f4f5335f
parent 74362 0135a0c77b64