src/HOL/Analysis/Regularity.thy
changeset 82313 df99e867c63e
parent 74362 0135a0c77b64