src/HOL/Analysis/Lipschitz.thy
changeset 77210 1ffee8893b12
parent 75455 91c16c5ad3e9
child 78131 1cadc477f644