src/HOL/Analysis/Continuous_Extension.thy
changeset 79961 2b9205301ff5
parent 78277 6726b20289b4