src/HOL/Analysis/Regularity.thy
changeset 73216 60c32e2c5577
parent 71633 07bec530f02e
child 74362 0135a0c77b64