src/HOL/Analysis/Regularity.thy
changeset 69448 51e696887b81
parent 69260 0a9688695a1b
child 69661 a03a63b81f44