src/HOL/Analysis/Lipschitz.thy
changeset 77830 0f2baf04b782
parent 75455 91c16c5ad3e9
child 78131 1cadc477f644