src/HOL/Analysis/Continuous_Extension.thy
changeset 66787 64b47495676d
parent 66289 2562f151541c
child 66884 c2128ab11f61