src/HOL/Analysis/Regularity.thy
changeset 69619 3f7d8e05e0f2
parent 69260 0a9688695a1b
child 69661 a03a63b81f44