src/HOL/Analysis/Lipschitz.thy
changeset 68050 7eacc812ad1c
parent 67979 53323937ee25
child 68240 fa63bde6d659
equal deleted inserted replaced
68045:ce8ad77cd3fa 68050:7eacc812ad1c