src/HOL/Analysis/Lipschitz.thy
changeset 75575 06f8b072f28e
parent 75455 91c16c5ad3e9
child 78131 1cadc477f644
equal deleted inserted replaced
75574:5945c6f5126a 75575:06f8b072f28e