src/HOL/Analysis/Analysis.thy
changeset 81387 c677755779f5
parent 79857 819c28a7280f