src/HOL/Analysis/Lipschitz.thy
changeset 75575 06f8b072f28e
parent 75455 91c16c5ad3e9
child 78131 1cadc477f644