src/HOL/Analysis/Lipschitz.thy
changeset 81275 5ed639c16ce7
parent 81142 6ad2c917dd2e