src/HOL/Analysis/Continuous_Extension.thy
changeset 67161 b762ed417ed9
parent 66884 c2128ab11f61
child 67613 ce654b0e6d69