src/HOL/Analysis/Lipschitz.thy
changeset 82313 df99e867c63e
parent 81142 6ad2c917dd2e