src/HOL/Analysis/Lipschitz.thy
changeset 74245 282cd3aa6cc6
parent 71698 b69dc6bcbea3
child 75455 91c16c5ad3e9