src/HOL/Analysis/Regularity.thy
changeset 72925 cd6f6e2fe99d
parent 71633 07bec530f02e
child 74362 0135a0c77b64