src/HOL/Analysis/Regularity.thy
changeset 68236 b4484ec4a8f7
parent 68046 6aba668aea78
child 68403 223172b97d0b