src/HOL/Analysis/Lipschitz.thy
changeset 77227 6c8c980e777a
parent 75455 91c16c5ad3e9
child 78131 1cadc477f644
equal deleted inserted replaced
77224:e3e326a2dab5 77227:6c8c980e777a