src/HOL/Analysis/Lipschitz.thy
changeset 74245 282cd3aa6cc6
parent 71698 b69dc6bcbea3
child 75455 91c16c5ad3e9
equal deleted inserted replaced
74244:12dac3698efd 74245:282cd3aa6cc6